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.
Keywords: embedded systems; safety; code generation; formalization
Proceedings of the 11th International Modelica Conference, Versailles, France, September 21-23, 2015
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.