Lucas Satabin
Esterel Technologies/ANSYS SBU, France
Jean-Louis Colaço
Esterel Technologies/ANSYS SBU, France
Olivier Andrieu
Esterel Technologies/ANSYS SBU, France
Bruno Pagano
Esterel Technologies/ANSYS SBU, France
Download article
http://dx.doi.org/10.3384/ecp15118637Published in: Proceedings of the 11th International Modelica Conference, Versailles, France, September 21-23, 2015
Linköping Electronic Conference Proceedings 118:68, p. 637-646
Published: 2015-09-18
ISBN: 978-91-7685-955-1
ISSN: 1650-3686 (print), 1650-3740 (online)
The ever growing requirement for safety in embedded systems, together with the willingness of having a modelling language to describe both the physics and the software that controls it makes Modelica an interesting candidate to design, simulate and implement complex systems. Originally designed to address multi-physics, since its version 3.3 Modelica integrates constructions to describe discrete controllers. Now the question of using Modelica to design critical embedded software arises.
In this paper we address the problem of defining a practical Modelica subset that can be entirely formalized and we sketch the formalization of this subset with a concrete example. This work should serve as a basis to define a suitable language that can be used to both simulate systems and generate embedded critical code.
David Broman, Peter Fritzson, and Sébastien Furic. Types in the modelica language. In Proceedings of the Fifth International Modelica Conference, 2006.
Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. A Conservative Extension of Synchronous Data-flow with State Machines. In EMSOFT’05, September 2005.
DO-178C. DO-178C Software Considerations in Airborne
Systems and Equipment Certification, December 2011.
DO-330. DO-330 Software Tool Qualification Considerations, December 2011.
DO-332. DO-332 Object-Oriented Technology and Related Techniques Supplement to DO-178C and DO-278A, December 2011.
Julien Forget, Frédéric Boniol, David Lesens, and Claire Pagetti. A multi-periodic synchronous data-flow language. In HASE 2008. 11th IEEE. IEEE, 2008.
Nicolas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. The synchronous dataflow programming language lustre. In Proceedings of the IEEE, 1991.
Atsushi Igarashi. Formalizing Advanced Class Mechanisms. PhD thesis, University of Tokyo, 1999.
Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight java: A minimal core calculus for java and gj. ACM Trans. Program. Lang. Syst., May 2001.
Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7), 2009.
Modelica Association. Modelica – A Unified Object-Oriented Language for Systems Modeling, version 3.3. http://modelica.org, May 2012.
Marc Pouzet. Lucid Synchrone, version 3. Tutorial and reference manual. Université Paris-Sud, LRI, April 2006.
Lucas Satabin, Olivier Andrieu, Bruno Pagano, and Jean-Louis Colaço. Formalization of A Modelica Subset for Safety-Critical Software Development. Technical report, Esterel Technologies, 2015.
Bernhard Thiele, Stefan-Alexander Schneider, and Pierre R Mai. A Modelica Sub-and Superset for Safety-Relevant Control Applications. In Proceedings of the Ninth International Modelica Conference, 2012.
