Sciweavers

Share
EMSOFT
2004
Springer

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

9 years 2 months ago
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...
Norman Scaife, Christos Sofronis, Paul Caspi, Stav
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where EMSOFT
Authors Norman Scaife, Christos Sofronis, Paul Caspi, Stavros Tripakis, Florence Maraninchi
Comments (0)
books