N. Scaife, C. Sofronis, P. Caspi, S. Tripakis and F. Maraninchi
Defining and translating a safe subset of Simulink/Stateflow into Lustre (2004)
Defining and translating a safe subset of Simulink/Stateflow into Lustre (2004)
TR-2004-16.pdf
Keywords: Model-based Design, Simulink, Stateflow, Lustre, Formal Methods, Safety-critical, Model-checking.
Abstract: 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.
