1 Introduction
The tool sf2lus is an (as yet) ad hoc translation from a subset of
Stateflow1 [1] into the synchronous
language Lustre [2].
The technical details of the translation can be found in the Verimag technical
report [3] and in the paper published in
EMSOFT'04 [4].
Here the sf2lus program is described which is the implementation of the
translator in Objective Caml.
This is designed to work with the s2l
translator [5] which translates a discrete-time subset of
Simulink into Lustre.
This package provides a script called ss2lus which calls the sf2lus
translator to extract the Stateflow component as Lustre nodes and provides
s2l with the information needed to incorporate the Stateflow Lustre
code into the output.
The sf2lus program can be used in isolation, however, to extract and test the
Stateflow components independently of the Simulink.
This requires a slightly different interface since constants and data imported
from Simulink or Matlab have to be defined locally and emulation is required
for other features such as the time variable t.
Output from the tool is primarily Lustre V4.
This version of Lustre includes bounded iteration using the when
construct in conjunction with statically-evaluated constants and proved very
useful in structuring Stateflow's unbounded iterations such as event broadcasts
and junction loops.
In general, however, it is intended that sf2lus be used in conjunction with
the planned Stateflow analysis tool to allow the elimination of unbounded
recursion either by automated transformation or by manual editing of the
Stateflow chart.
Other outputs include preliminary versions of SCADE [6] which
allows Stateflow charts to be included as source code into the SCADE
suite of tools by Esterel Technologies, Inc., Reluc which is a commercial version of
Lustre also by Esterel and some minor support required by the abstract
interpretation tool Nbac (via lus2nbac provided in the Lustre
distribution).
These output formats are only partially supported, however.
Note that the Lustre output itself can be used as input to a variety of tools
including the model-checker Lesar [7].