Communication by asynchronous messages - different queuing disciplines

The semantics of FSM modeling

A Finite State Machine (FSM) of Mealy style is a state machine as in UML, where a transition has normally an input and a subsequent output (in addition to the transfer to the next state). Such a transition is like two IOA transition, first an input transition leading to an intermediate state, and then an output transition leading to the next state of the FSM. In the intermediate state, the machine does not accept any other input, it simple prepares for the output transition. In the case of an Extended FSM (as in UML), the transition may also be associated with some update of local variables and the calculation of the effective values of the output parameters.

In the modeling paradigm of Communicating FSMs, the input messages for a given FSM are first placed into an input queue before they are processed by the FSM through the execution of an appropriate transition. There are different queueing disciplines that can be used, such as the following,. Note that we consider a general system architecture which contains many FSMs that communicate with one another.

Another semantic variation point (see UML) is the question how unspecified receptions are handled. The following cases are the most popular:

In many papers on more theoretical aspects of FSMs, state machines with input queues are described in a formalism that resembles IOA. I will call this approach FSM in IOA notation. With this approach each input-output transition is cut into two transitions, one input and one output. In contrast to the normal FSM semantics, the state after the input transition is a normal state (and not an intermediate state with special properties). This means after an input, another input may be received. Also from a given state, there may be several output transitions - and the machine will have to choose which one to executed (an internal choice). There may also be so-called mixed states from which input and output transitions are possible - this means in this state, the machine may macke a choice between doing an output or processing an input (or if none is present, wait for a while for an input - if none arrives, the basic liveness assumptions requires that finally an output transition must be performed).

The modeling paradigm of FSM in IOA notation is more powerful than the standard FSM modeling paradigm. Therefore the latter is sometimes extended by introducing spontaneous transitions (without input) that may produce output. Such FSM then, may include mixed states as the FSMs in IOA notation.

Here are some examples with input alphabet {b, c} and output alphabet {a, d, e} - the notation - means output and + means input. The first two machine have equivlent behavior, that is, admit the same set of traces.

two FSMs Gouda

Reachability analysis

The reachability analysis for a system of FSMs is similar as for a system of IOA. The main differences are the following:

We do not discuss the reachability analysis for all the different semantic variation points that exists for the Communicating FSM model. We describe in the following only the case of two FSM is IOA notation with single FIFO queues. The following text is similar to the definition of reachability analysis given for the IOA modeling paradigm. The changed part of written in blue.

The composition of two FSM models, C1 and C2, with alphabets A1 = I1 union O1, and A2 = I2 union O2, respectively, can be modeled by a global LTS that represents the behavior of these two component FSM and their interactions, in the following called C. The model of C is the following LTS (Note: rules (1) and (2) are the same as for LTS):

  1. The states of C are of the form <s1, q21, q12, s2>, where s1 is a state of C1 and s2 is a state of C2, and q12 and q21 are the queues of C2 and C1, respectively.
  2. The initial state of C is the set of states <s1-initial, empty, empty, s2-initial> where si-initial are initial states of Ci (i = 1, 2).
  3. The transitions of C from a state <s1, q21, q12, s2> are the following:

Example of reachability analysis

We first consider the third state machine above communicating with its "mirror image", and assuming that IAO communication is used (directly coupled transitions without queuing):

ex 1

Machine A . . . . . . . . . . . . . . . . . .. . . . Machine B . . . . . . . . . . . . . . . . . . . . The global system

Now we consider that the two machines communicate with message queuing (that is, like FSM in IOA notation). Here is the global reachability grapb (partial, since the queue length of the second machine is not bounded - therefore the number of possible global states is infinite). The notation (s1, q1, q2, s2) means that the first machine is in state s1 and the content of its input queues is q1, and similarly for the second machine. Note that in the global state marked *, there are two unspecified receptions, and the global state marked + is a deadlock - however, this is probably a desired final state, since both communicating machines, are in their respective final state (the only state with no further transitions).

two machines ex 2

Results of reachability analysis

Reachability analysis allows us to obtain a description of the global behavior of the system that is defined as the composition of several components, each with its specified behavior. For this global behavior, we are interested in two aspects:

Example of system development: See course notes for SEG-2106 , Chapter 3 R - Section: "Sub-systems communicating by message passing"

History of protocol engineering C

The first paper that used state machine modeling of communication protocols was probably the paper describing the Alternating Bit Protocol (ABP) in 1968. My paper of 1978 on Finite State Description of Communication Protocols was the first paper to introduce reachability analysis for verifying that a given protocol and underlying message transmission service provides a given service specification (in this case, reliable data transfer to the sender to the receiver). I used the APB as the main example, but also treated the X.25 protocol which was then the official ITU standard for computer communication over data networks. At the same time, Colin West with colleagues from the IBM Zurich Research Lab had also developed methods for checking that protocol specifications have no deadlock nor unspecified reception, also using reachability analysis based on state machine models (see paper of 1980). They introduced the notion of unspecified reception. All these papers used the modeling paradigm of FSM in IOA notation (see above). During those days, various formalisms were used to describe protocols (see survey of 1980).

An overview of the history of protocol engineering, including the development of the first protocols for computer networks in the 1970ies, is given in my paper Some notes on the history of protocol engineering (or a shortened version with the ABP example). These principles of protocol engineering were applied to a large extend during the standardization development for Open Systems Interworking (OSI) during the 1980ies (see my paper Protocol Specification for OSI from 1990) - however, these protocols were never much used because they were superseded by the wide-spread use of the Internet protocols in the 1990ies.

In the late 1970ies, Colin West, with his colleagues at IBM, developed in interesting reachability analysis tool that helped the protocol designer defining protocols without unspecified receptions (see paper of 1980). Using this tool, the designer could develop the behavior of two (or more) state machines interactively by introducing sending transitions from the different states of the machines. The tool will determine automatically in which state (or states) of the destination machine each output message could be received. These receptions are indicated by the tool, and the designer has to select the state that should be entered after the reception of the message (either a state that already exists, or a new state for the machine in question). Thus, all possible receptions must be handled by the designer and the resulting design will have no unspecified reception. Deadlocks were also detected by the tool - they can be resolved by introducing an output transition in one of the machine states involved in the deadlock - but this is not necessarily a good solution (one may also change the earlier behavior of one of the involved state machines).

Created: October 9, 2014, revised Oct. 2015