We have got a fist cut of a state machine language. Our languages supports the declaration of in- and out events, entry and exit actions for states, transitions between states with guard conditions and transition actions. In-events are transmitted from the environment into the state machine while with out-events the machine can notify its environment. Both event types have optional parameters. In addition, a state machine can define local variables. Similar to components, state machines can be instantiated multiple times.
State machines are logically independent entities which can be embedded in different contexts. We have already built an integration with ordinary modules as well as components, so state machines can be embedded into modules and components. Dependent on their environment, they can bind their out events to either a regular C function call, a call to an operation provided by a client-server interface or a message which is sent through a message interface of a required port.
We also started with building an integration with the NuSMV model checker which supports static verification of the correctness of a state machine. One very important feature here is that a state machine can be verified independently from where it’s embedded. This is possible because a state machine’s internal behavior only depends on the events and not on their bindings.