Timothy Bourke
Francois Carcenac
Abstract
Hybrid systems modelers like Simulink come with a rich collection of discrete-time and continuous-time blocks. Most blocks are not defined in terms of more elementary ones—and some cannot be—but are instead written in imperative code and explained informally in a reference manual. This raises the question of defining a minimal set of orthogonal programming constructs such that most blocks can be programmed directly and thereby given a specification that is mathematically precise, and whose compiled version performs comparably to handwritten code.
In this paper, we show that a fairly large set of blocks of a standard library like the one provided by Simulink can be programmed in a precise, purely functional language using stream equations, hierarchical automata, Ordinary Differential Equations (ODEs), and deterministic synchronous parallel composition. Some blocks cannot be expressed in our setting as they mix discrete-time and continuous-time signals in unprincipled ways that are statically forbidden by the type checker.
The experiment is conducted in Zélus, a synchronous language that conservatively extends Lustre with ODEs to program systems that mix discrete-time and continuous-time signals.
- Rajeev Alur. 2011. Formal Verification of Hybrid Systems. In Proceedings of the 9th ACM International Conference on Embedded Software (EMSOFT). ACM, Taipei, Taiwan, 273--278. Google Scholar
Digital Library
- Karl J. Åström and Richard M. Murray. 2008. Feedback Systems: An Introduction for Scientists and Engineers. Princeton University Press, NJ, USA. Google ScholarDigital Library
- Albert Benveniste, Timothy Bourke, Benoit Caillaud, Bruno Pagano, and Marc Pouzet. 2014. A Type-based Analysis of Causality Loops in Hybrid Systems Modelers. In Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (HSCC). ACM, Berlin, Germany, 71--82. Google ScholarDigital Library
- Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet. 2011. A Hybrid Synchronous Language with Hierarchical Automata: Static Typing and Translation to Synchronous Code. In Proceedings of the 9th ACM International Conference on Embedded Software (EMSOFT). ACM, Taipei, Taiwan, 137--147. Google ScholarDigital Library
- Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet. 2011. Divide and recycle: types and compilation for a hybrid synchronous language. In Proceedings of the ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools and Theory for Embedded Systems (LCTES). ACM, Chicago, USA, 61--70. Google ScholarDigital Library
- Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet. 2012. Non-Standard Semantics of Hybrid Systems Modelers. Journal of Computer and System Sciences (JCSS) 78, 3 (May 2012), 877--910. Special issue in honor of Amir Pnueli. Google ScholarDigital Library
- Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicolas Halbwachs, Paul Le Guernic, and Robert de Simone. 2003. The synchronous languages 12 years later. Proc. IEEE 91, 1 (Jan. 2003), 64--83.Google ScholarCross Ref
- Gérard Berry. 1989. Real time programming: Special purpose or general purpose languages. Information Processing 89 (1989), 11--17.Google Scholar
- Olivier Bouissou and Alexandre Chapoutot. 2012. An operational semantics for Simulink’s simulation engine. In Proceedings of the 13th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, Tools and Theory for Embedded Systems (LCTES). ACM, Beijing, China, 129--138. Google ScholarDigital Library
- Timothy Bourke, Jean-Louis Colaço, Bruno Pagano, Cédric Pasteur, and Marc Pouzet. 2015. A Synchronous-based Code Generator For Explicit Hybrid Systems Languages. In Proceedings of the 24th International Conference on Compiler Construction (CC) (Lecture Notes in Computer Science). Springer, London, UK, 69--88.Google ScholarCross Ref
- Timothy Bourke and Marc Pouzet. 2013. Zélus, a Synchronous Language with ODEs. In Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC). ACM, Philadelphia, USA, 113--118. Google ScholarDigital Library
- Luca Carloni, Maria D. Di Benedetto, Alessandro Pinto, and Alberto Sangiovanni-Vincentelli. 2004. Modeling Techniques, Programming Languages, Design Toolsets and Interchange Formats for Hybrid Systems. Technical Report. IST-2001-38314 WPHS, Columbus Project.Google Scholar
- Jean-Louis Colaço and Marc Pouzet. 2004. Type-based Initialization Analysis of a Synchronous Data-flow Language. International Journal on Software Tools for Technology Transfer (STTT) 6, 3 (August 2004), 245--255.Google ScholarCross Ref
- M. Dowell and P. Jarratt. 1972. A modified regula falsi method for computing the root of an equation. BIT Numerical Mathematics 11, 2 (June 1972), 168--174.Google Scholar
- Esterel Technologies SAS 2016. Gateway Guidelines for Simulink. Esterel Technologies SAS.Google Scholar
- John T. Feo, David C. Cann, and Rodney R. Oldehoeft. 1990. A report on the Sisal language project. J. Parallel and Distrib. Comput. 10 (1990), 349--366. Google ScholarDigital Library
- Léonard Gérard, Adrien Guatto, Cédric Pasteur, and Marc Pouzet. 2012. A Modular Memory Optimization for Synchronous Data-Flow Languages. Application to Arrays in a Lustre Compiler. In Proceedings of the 13th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers and Tools for Embedded Systems (LCTES). ACM, Beijing, 51--60. Google ScholarDigital Library
- Nicolas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. 1991. The Synchronous Dataflow Programming Language Lustre. Proc. IEEE 79, 9 (September 1991), 1305--1320.Google ScholarCross Ref
- Grégoire Hamon. 2005. A denotational semantics for Stateflow. In Proceedings of the 5th ACM International Conference on Embedded Software (EMSOFT). ACM, Jersey City, NJ, USA, 164--172. Google ScholarDigital Library
- Gregoire Hamon and John Rushby. 2004. An Operational Semantics for Stateflow. In Proceedings of the 7th International Conference on Fundamental Approaches to Software Engineering (FASE) (Lecture Notes in Computer Science), Vol. 2984. Springer, Barcelona, Spain, 229--243.Google ScholarCross Ref
- Alan C. Hindmarsh and Radu Serban. 2016. User Documentation for cvode v2.9.0 (v2.9.0 ed.). Lawrence Livermore National Laboratory, Livermore, CA, USA.Google Scholar
- Edward A. Lee and Haiyang Zheng. 2005. Operational Semantics of Hybrid Systems. In Proceedings of the 8th International Conference on Hybrid Systems: Computation and Control (HSCC) (Lecture Notes in Computer Science), Vol. 3414. Springer, Zurich, Switzerland, 25--53. Google ScholarDigital Library
- Oded Maler, Zouar Manna, and Amir Pnueli. 1992. From Timed to Hybrid Systems. In Proceedings of the REX Workshop Real-Time: Theory in Practice (Lecture Notes in Computer Science), Vol. 600. Springer, Mook, The Netherlands, 447--484. Google ScholarDigital Library
- Lionel Morel. 2007. Array Iterators in Lustre: From a Language Extension to Its Exploitation in Validation. EURASIP Journal on Embedded Systems 2007, 1 (2007), article 059130.Google ScholarCross Ref
- Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, and Serge Torres. 2010. Handbook of Floating-Point Arithmetic. Birkhäuser, Basel, Switzerland. Google Scholar
- B. C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA, USA. Google ScholarDigital Library
- Kohei Suenaga, Hiroyoshi Sekine, and Ichiro Hasuo. 2013. Hyperstream Processing Systems: Nonstandard Modeling of Continuous-time Signals. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, New York, NY, USA, 417--430. Google ScholarDigital Library
- Stavros Tripakis, Christos Sofronis, Paul Caspi, and Adrian Curic. 2005. Translating Discrete-Time Simulink to Lustre. ACM Transactions on Embedded Computing Systems 4 (2005), 779--818. Issue 4. Special Issue on Embedded Software. Google ScholarDigital Library
- Stavros Tripakis, Christos Stergiou, Chris Shaver, and Edward A. Lee. 2013. A modular formal semantics for Ptolemy. Mathematical Structures in Computer Science 23, 4 (008 2013), 834--881.Google Scholar
Index Terms
- A Synchronous Look at the Simulink Standard Library
Recommendations
A hybrid synchronous language with hierarchical automata: static typing and translation to synchronous code
EMSOFT '11: Proceedings of the ninth ACM international conference on Embedded softwareHybrid modeling tools like Simulink have evolved from simulation platforms into development platforms on which testing, verification and code generation are also performed. It is critical to ensure that the results of simulation, compilation and ...
Building a hybrid systems modeler from synchronous language principles
EMSOFT '15: Proceedings of the 12th International Conference on Embedded SoftwareHybrid systems modeling languages are widely used in the development of embedded systems. Two representatives are Simulink/Stateflow1 that combine Ordinary Differential Equations (ODEs), data-flow and difference equations, hierarchical automata a la ...
Zélus: a synchronous language with ODEs
HSCC '13: Proceedings of the 16th international conference on Hybrid systems: computation and controlZélus is a new programming language for modeling systems that mix discrete logical time and continuous time behaviors. From a user's perspective, its main originality is to extend an existing Lustre-like synchronous language with Ordinary Differential ...
Comments