Defining and translating a "safe" subset of simulink/stateflow into lustre

The Simulink/Stateflow toolset is an integrated suite enabling model-based design and has become popular in the automotive and aeronautics industries. We have previously developed a translator called s2l from Simulink to the synchronous language Lustre and we build upon that work by encompassing Stateflow as well. Stateflow is problematical for synchronous languages because of its unbounded behaviour so we propose analysis techniques to define a subset of Stateflow for which we can define a synchronous semantics. We go further and define a "safe" subset of Stateflow which elides features which are potential sources of errors in Stateflow designs. We give an informal presentation of the Stateflow to Lustre translation process and show how our model-checking tool Lesar can be used to verify some of the semantical checks we have proposed. Finally, we present a small case-study. Categories and Subject Descriptors: D.2.2 [Design Tools and Techniques]: Computer-aided software engi...

• Type: Conference
• Year: 2004
• Where: EMSOFT
• Authors: Norman Scaife, Christos Sofronis, Paul Caspi, Stavros Tripakis, Florence Maraninchi
• Keywords: EMSOFT 2004, Software Engineering, Stateflow, Synchronous Language Lustre, Synchronous Languages