System modeling using state machines

A. Building a model

B. Checking properties of a given model

C. Comments on non-determinism in models

A model is non-deterministic if it allows for several behaviors. Such non-determinism is often intended, because at the more abstract level one wants to leave several behavior options, or it is known that certain aspects of the behavior cannot be determined, for instance, due to unknown speed of execution of the different parallel processes inside the system. Here are some examples.

  1. Non-determined sequencing defined by a sequence diagram. Diagram (a) below defines a single sequence of interactions, namely the following: send a, receive a, send c, receive c, send b, receive b, send d, receive d. However, Diagram (b) implies many different orders for the primitive send and receive operations, because the relative order of send a, and send c is not defined; similarly the order between receive a and send b is not defined. One says that the diagram shows a partial order, for instance, the order first receive b, then send d is clearly there in this diagram.
  2. Non-determinism due to different execution speeds. The two FSM models below, when executed jointly with message passing between them, could give rise to an execution sequence corresponding to the second sequence diagram above. (Note: The transitions labelled "!xx" represent spontaneous transitions, only the output xx is indicated; the transitions labelled "?xx" are trigged by the input xx - they have no output.) However, if the speed of transmission of the message c would be faster, or the execution speed of machine A slower, the message c may arrive when the machine A is in state 2. This would be an unspecified reception (the reception of this message is not defined in this state; this must be considered a design error). We conclude that the design of the machines A and B shown below is bad.
  1. Non-deterministic machine behavior.

Created: December 17, 2008; last update: January 20, 2008