Defining and translating a" safe" subset of Simulink/Stateflow into Lustre

N Scaife, C Sofronis, P Caspi, S Tripakis… - Proceedings of the 4th …, 2004 - dl.acm.org
N Scaife, C Sofronis, P Caspi, S Tripakis, F Maraninchi
Proceedings of the 4th ACM international conference on Embedded software, 2004dl.acm.org
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 Simtolus 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 …
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 Simtolus 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.
ACM Digital Library
以上显示的是最相近的搜索结果。 查看全部搜索结果