Specification languages: Programming languages, Extended state machine models and Petri nets

In the above chapters we have discussed basic state machine models which lead to global states with a finite number of states, except when input queues are unbounded. However, their simplicity is often not powerful enough to model all aspects of the system to be described. There are two solutions to this problem:

An extended state machine model and a programing model have many similarities:

However, behavior specifications for communication protocols and system requriements, in general, are often nondeterministic (in a given state, different outputs may be produced, or the values of certain output messages may be underfined). On the contrary, normal programming languages are normally deterministic. Also, programming languages are often quite complex, and the defined behavior may not be clear to the reader.

For these reasons, Dijkstra proposed in 1975 the Guarded Command Language (see Wikipedia) which is very simple and helps the understanding (and possibly proving) of properties of a given program. This language was later adapted by Holzmann in the Promela language which is used with Spin.

Petri nets also represent a generalization of the basic state machine models of LTS and IOA. A single Petri net may model several concurrent activities (there may be several tokens simultaneously within the given Petri net), as well as data flow between them or mutual exclusion for shared resources. Message passing can be modeled by a token which goes from one place of the Petri net to another place - each place holds only messages of a given type. - In order to model messages with parameters, Petri nets have also be extended, and are called Colored Petri Nets, Predicate Transition Nets, or similar. These extensions are as follows:

We note that the formalism of extended Petri nets has been used to define the semantics of UML Activity Diagrams. The explanation of their semantics talks about tokens that go from one activity to the next. These tokens may represent data flow, in which case one would consider extended Petri-net tokens with parameters. See example below.

AD semantics

Created: October 2014