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

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

REFERENCES

• 1: C. Banphawatthanarak, B. H. Krogh, and K. Butts. Symbolic verification of executable control specifications. In Proc. of the Tenth IEEE International Symposium on Computer Aided Control System Design, pages 581--586, Hawaii, Aug 1999.
• 2: S. Bensalem, V. Ganesh, Y. Lakhnech, C. M. Noz, S. Owre, H. Rueß, J. Rushby, V. Rusu, H. Saïdi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. In C. M. Holloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop, pages 187--196, Hampton, VA, Jun 2000.
• 3: Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V]
• 4: P. Caspi, A. Curic, A. Maignan, C. Sofronis, and S. Tripakis. Translating discrete-time Simulink to Lustre. In R. Alur and I. Lee, editors, EMSOFT'03, LNCS. Springer Verlag, 2003.
• 5: Paul Caspi , Adrian Curic , Aude Maignan , Christos Sofronis , Stavros Tripakis , Peter Niebert, From simulink to SCADE/lustre to TTA: a layered approach for distributed embedded applications, Proceedings of the 2003 ACM SIGPLAN conference on Language, compiler, and tool for embedded systems, June 11-13, 2003, San Diego, California, USA
• 6: Ford. Structured Analysis Using Matlab/Simulink/Stateflow - Modeling Style Guidelines. Technical report, Ford Motor Company, 1999.
• 7: N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data-flow programming language LUSTRE. Proc. of the IEEE, 79(9):1305--1320, September 1991.
• 8: Nicolas Halbwachs , Fabienne Lagnier , Pascal Raymond, Synchronous Observers and the Verification of Reactive Systems, Proceedings of the Third International Conference on Methodology and Software Technology: Algebraic Methodology and Software Technology, p.83-96, June 21-25, 1993
• 9: G. Hamon and J. Rushby. An operational semantics for stateflow. In Proc. of Fundamental Approaches to Software Engineering, Barcelona, Spain, March 2004.
• 10: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 11: Bertrand Jeannet , Nicolas Halbwachs , Pascal Raymond, Dynamic Partitioning in Analyses of Numerical Properties, Proceedings of the 6th International Symposium on Static Analysis, p.39-50, September 22-24, 1999
• 12: Gerald Lüttgen , Michael von der Beeck , Rance Cleaveland, A compositional approach to statecharts semantics, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.120-129, November 06-10, 2000, San Diego, California, United States
• 13: Florence Maraninchi , Nicolas Halbwachs, Compiling ARGOS into Boolean Equations, Proceedings of the 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.72-89, September 09-13, 1996
• 14: F. Maraninchi and Y. Rémond. Argos: an Automaton-Based Synchronous Language. Computer Languages, (27):61--92, 2001.
• 15: Erich Mikk , Yassine Lakhnech , Michael Siegel, Hierarchical Automata as Model for Statecharts, Proceedings of the Third Asian Computing Science Conference on Advances in Computing Science, p.181-196, December 09-11, 1997
• 16: N. Scaife, C. Sofronis, P. Caspi, S. Tripakis, and F. Maraninchi. Defining and translating a ``safe'' subset of Simulink/Stateflow into Lustre. Technical Report TR-2004-16, http://www-verimag.imag.fr.
• 17: Mary Sheeran , Satnam Singh , Gunnar Stålmarck, Checking Safety Properties Using Induction and a SAT-Solver, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.108-125, November 01-03, 2000
• 18: A. Tiwari. Formal semantics and analysis methods for Simulink Stateflow models. Technical report, http://www.csl.sri.com/~tiwari/stateflow.html.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Computer-aided software engineering (CASE)

General Terms:
Design, Languages, Reliability, Verification

Keywords:
automatic translation, embedded software, lustre, simulink