Translating discrete-time simulink to lustre

ABSTRACT

We present a method of translating discrete-time Simulink models to Lustre programs. Our method consists of three steps: type inference, clock inference, and hierarchical bottom-up translation. In the process, we explain and formalize the typing and timing mechanisms of Simulink. The method has been implemented in a prototype tool called S2L, which has been used in the context of a European research project to translate two automotive controller models provided by Audi.

REFERENCES

• 1: Agrawal, A., Simon, G., and Karsai, G. 2004. Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations. In Workshop on Graph Transformation and Visual Modeling Techniques, Barcelona, Spain.
• 2: Åström, K. and Wittenmark, B. 1984. Computer Controlled Systems. Prentice-Hall, Englewood Cliffs, NJ.
• 3: Paul Caspi, Clocks in dataflow languages, Theoretical Computer Science, v.94 n.1, p.125-140, March 1992 [doi>10.1016/0304-3975(92)90326-B]
• 4: P. Caspi , D. Pilaud , N. Halbwachs , J. A. Plaice, LUSTRE: a declarative language for real-time programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.178-188, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41641]
• 5: Paul Caspi , Marc Pouzet, Synchronous Kahn networks, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.226-238, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 6: Caspi, P., Curic, A., Maignan, A., Sofronis, C., and Tripakis, S. 2003a. Translating discrete-time Simulink to Lustre. In Embedded Software (EMSOFT'03). LNCS, Vol. 2855. Springer, NY.
• 7: 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
• 8: Cervin, A., Henriksson, D., Lincoln, B., and Årzén, K.-E. 2002. Jitterbug and Truetime: Analysis tools for real-time control systems. In 2nd Workshop on Real-Time Tools.
• 9: Chutinan, A. and Krogh, B. 2003. Computational techniques for hybrid system verification. IEEE Trans. Automatic Control 48, 1.
• 10: Colaço, J. and Pouzet, M. 2003. Clocks as first class abstract types. In Embedded Software (EMSOFT'03). LNCS, Vol. 2855. Springer, NY.
• 11: Guernic, P. L., Gautier, T., Borgne, M. L., and Maire, C. L. 1991. Programming real-time applications with Signal. Proc. of the IEEE 79, 9, 1321--1336.
• 12: Halbwachs, N., Caspi, P., Raymond, P., and Pilaud, D. 1991. The synchronous dataflow programming language Lustre. Proceedings of the IEEE 79, 9 (Sept.).
• 13: Nicolas Halbwachs , Yann-Erick Proy , Patrick Roumanoff, Verification of Real-Time Systems using Linear Relation Analysis, Formal Methods in System Design, v.11 n.2, p.157-185, Aug. 1997 [doi>10.1023/A:1008678014487]
• 14: Thomas A. Henzinger , Benjamin Horowitz , Christoph Meyer Kirsch, Giotto: A Time-Triggered Language for Embedded Programming, Proceedings of the First International Workshop on Embedded Software, p.166-184, October 08-10, 2001
• 15: Paul Hudak , Simon Peyton Jones , Philip Wadler , Brian Boutel , Jon Fairbairn , Joseph Fasel , María M. Guzmán , Kevin Hammond , John Hughes , Thomas Johnsson , Dick Kieburtz , Rishiyur Nikhil , Will Partain , John Peterson, Report on the programming language Haskell: a non-strict, purely functional language version 1.2, ACM SIGPLAN Notices, v.27 n.5, p.1-164, May 1992 [doi>10.1145/130697.130699]
• 16: Jersak, M., Ziegenbein, D., Wolf, F., Richter, K., Ernst, R., Cieslog, F., Teich, J., Strehl, K., and Thiele, L. 2000. Embedded system design using the SPI workbench. In Proc. of the 3rd International Forum on Design Languages.
• 17: Joisha, P. and Banerjee, P. 2003. The MAGICA type inference engine for MATLAB. In Compiler Construction (CC). LNCS 2622, Springer, NY.
• 18: Kahn, G. 1974. The semantics of a simple language for parallel programming. In Proc. of the IFIP Congress.
• 19: Christoph Meyer Kirsch , Marco A. A. Sanvido , Thomas A. Henzinger , Wolfgang Pree, A Giotto-Based Helicopter Control System, Proceedings of the Second International Conference on Embedded Software, p.46-60, October 07-09, 2002
• 20: Hermann Kopetz, Real-Time Systems: Design Principles for Distributed Embedded Applications, Kluwer Academic Publishers, Norwell, MA, 1997
• 21: Hermann Kopetz , Günter Grünsteidl, TTP-A Protocol for Fault-Tolerant Real-Time Systems, Computer, v.27 n.1, p.14-23, January 1994 [doi>10.1109/2.248873]
• 22: Lee, E. and Messerschmitt, D. 1987. Synchronous data flow. Proceedings of the IEEE 75, 9, 1235--1245.
• 23: Lee, E. and Parks, T. 1995. Dataflow process networks. Proceedings of the IEEE 83, 5 (May), 773--799.
• 24: Alberto Martelli , Ugo Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.258-282, April 1982 [doi>10.1145/357162.357169]
• 25: Milner, R. 1978. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17, 384--375.
• 26: Neema, S. 2001. Simulink and Stateflow data model. Tech. rep., ISIS, Vanderbilt University, Nashville, TN.
• 27: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 28: Christophe Ratel , Nicolas Halbwachs , Pascal Raymond, Programming and verifying critical systems by means of the synchronous data-flow language LUSTRE, Proceedings of the conference on Software for citical systems, p.112-119, December 04-06, 1991, New Orleans, Louisiana, United States
• 29: P. Raymond , X. Nicollin , N. Halbwachs , D. Weber, Automatic Testing of Reactive Systems, Proceedings of the IEEE Real-Time Systems Symposium, p.200, December 02-04, 1998
• 30: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 31: N. Scaife , P. Caspi, Integrating Model-Based Design and Preemptive Scheduling in Mixed Time- and Event-Triggered Systems, Proceedings of the 16th Euromicro Conference on Real-Time Systems (ECRTS'04), p.119-126, June 30-July 02, 2004 [doi>10.1109/ECRTS.2004.15]
• 32: N. Scaife , C. Sofronis , P. Caspi , S. Tripakis , F. Maraninchi, Defining and translating a "safe" subset of simulink/stateflow into lustre, Proceedings of the 4th ACM international conference on Embedded software, September 27-29, 2004, Pisa, Italy [doi>10.1145/1017753.1017795]
• 33: Silva, B., Richeson, K., Krogh, B., and Chutinan, A. 2000. Modeling and verifying hybrid dynamical systems using CheckMate. In ADPM.
• 34: Steve Sims , Rance Cleaveland , Ken Butts , Scott Ranville, Automated Validation of Software Models, Proceedings of the 16th IEEE international conference on Automated software engineering, p.91, November 26-29, 2001
• 35: Tiwari, A. 2002. Formal semantics and analysis methods for Simulink Stateflow models. Tech. rep., SRI International.
• 36: Stéphane Tudoret , Simin Nadjm-Tehrani , Albert Beneviste , Jan-Erik Strömberg, Co-simulation of Hybrid Systems: Signal-Simulink, Proceedings of the 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.134-151, September 20-22, 2000

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques

Additional Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.4 Model Validation and Analysis

General Terms:
Design, Languages, Reliability, Verification

Keywords:
Code generation, Lustre, Simulink, embedded software