Up Next

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].

Up Next