State-Machines and Code Generation

From Event-B
Revision as of 06:49, 16 May 2012 by imported>Andy
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Generating Code from State-Machine Diagrams

We introduce the ability to generate code from state-machine diagrams in version 0.2.3 of the code generation feature plug-in. Code is generated from the diagram itself, and no additional mark-up of the model is required; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-machine(s) are created in a machine using the existing state-machine plug-in, subject to the limitations described below.

Limitations/What Can Be Translated

The current code generation tool is restricted to generating code for a single Event-B machine containing one or more state-machines. We have yet to explore the decomposition/composition of machines containing state-machines.

We do not handle nested state-machines.

Translations

Diagram here

Enumeration of states.

Initial state

Single outgoing transition

Multiple Outgoing transitions

Tooling

TODO - list