s2c (Stateflow 2 Circus)

s2c is a tool that reads Stateflow models (in .mdl format) and calculates their Circus semantics. It can be downloaded here.

A number of examples modelled in Stateflow along with their Circus semantics can be found here.

The Circus semantics of Stateflow models depends on:

• basic definitions [ LaTeX ];
• model of the simulator [ LaTeX | PDF ]

The formalisation of the translation implemented in this tool is available here:

• Formal syntax of Stateflow: StateflowAbstractSyntax.tex, StateflowAbstractSyntax.pdf;
• Formal syntax of Z: ZFormalSyntax.tex, ZFormalSyntax.pdf;
• Formal syntax of Circus: CircusFormalSyntax.tex, CircusFormalSyntax.pdf;
• Formal translation rules: Stateflow2Circus.tex, Stateflow2Circus.pdf.

Further examples:

• shift logic
  1. .mdl file: sf_car.mdl;
  2. Circus model: sf_car.tex, sf_car.pdf;
  3. Function library for specification sf_car.tex: calc_th.tex, calc_th.pdf.
• fan controller
  1. .mdl file: air.mdl;
  2. Circus model: air_Controller_model.tex, air_Controller_model.pdf;
  3. Source files for a parallel implementation: parallel_implementation.zip;
  4. Circus model of the implementation: air_Controller_impl_model.tex, air_Controller_impl_model.pdf.

Publications: