An example

In this section, we will use an example TTM called SAMPLE to illustrate the workings of the verifier. SAMPLE is a single simple TTM, i.e. it is not the parallel composition of many TTMs.

An example involving the parallel composition of processes, and using shared variables, may be found in [#Ost92a##1###]. VERIFY has a <#76#>compose<#76#> command which allows for TTMs to be composed in parallel. It allows for the possibility of both (a) shared variables, and (b) shared transitions. Thus, both asynchronous and synchronous communication can be modelled. Concurrent and nondeterministic behaviour can also be represented. TTMs can model most features of real-time programs, Petri Nets, Statecharts and Communicating Sequential Processes. In particular, TTMs have data variables that can be used to represent program variables, arrays, records and other data structures.