A first cut at statemachines

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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s