Modeling State Machines with Protocols

This guide shows how to map a state machine diagram onto a set of Flex local protocols using do tail statements. For the reference on protocol statement forms, see Flex Protocols Reference.

State machine diagrams are a popular way of modeling software behavior. Technically speaking, any machine with a state that changes over time is a state machine. However, in systems engineering, a state machine usually refers to a graph-like diagram that depicts a set of disjoint states connected by transitions. Below is such a diagram depicting states of a hypothetical controller component on an aircraft:

Flex is able to express behavior in a way that cleanly maps to and from a state machine diagram. The behavior of each state can be modeled as a local protocol, and a state transition corresponds to the execution of a do tail statement:

component AircraftController;

local protocol initializing in AircraftController {
  // initialization work ...
  do tail standby;
}

local protocol standby in AircraftController {
  // wait for execution or finalize signal ...
  branch
  | true => do tail executing;
  | true => do tail finalizing;
  end
}

local protocol executing in AircraftController {
  // execution work ...
  // wait for standby or finalize signal ...
  branch
  | true => do tail standby;
  | true => do tail finalizing;
  end
}

local protocol finalizing in AircraftController {
  // finalization work ...
}

To run the model checker on a Flex specification that contains do or do tail statements, only the initial state should be included in the system:

system aircraftSystem { initializing; /* protocols for other components */ }

State machine diagrams are good at expressing high-level relationships between states of a protocol. However, they are usually very bad at including lower-level details. In the state machine diagram above, it is unspecified what exactly the aircraft controller should be doing while in each state. Low-level information is often defined separately from the high-level state diagrams with little to no connection defined between them.

Flex does not have this problem because both the high-level information of state transitions and the low-level information of computation are expressed in the same language. A do tail statement is just another protocol statement like send, var, or set. The only difference is that we have chosen to understand do tail as a state transition and the other statements as lower-level computation.