A New Formalism for Modeling of Reactive and Hybrid Systems

Martin Otter
German Aerospace Centre (DLR), Institute for Robotics and Mechatronics, Germany

Martin Malmheden
Dassault Systèmes, Lund, Sweden

Hilding Elmqvist
Dassault Systèmes, Lund, Sweden

Sven Erik Matsson
Dassault Systèmes, Lund, Sweden

Charlotta Johnsson
Department of Automatic Control, Lund University, Sweden

Ladda ner artikelhttp://dx.doi.org/10.3384/ecp09430108

Ingår i: Proceedings of the 7th International Modelica Conference; Como; Italy; 20-22 September 2009

Linköping Electronic Conference Proceedings 43:41, s. 364-377

Visa mer +

Publicerad: 2009-12-29

ISBN: 978-91-7393-513-5

ISSN: 1650-3686 (tryckt), 1650-3740 (online)


A new Modelica library is presented that is used to model safe hierarchical state machines in combination with any Modelica model; e.g.; controllers; logical blocks; and physical systems described by differential-algebraic equations. It has been designed to simplify usage; improve safety aspects and to harmonize with the design of the new Modelica_ EmbeddedSystems library. Furthermore; new blocks are introduced to define actions in a visual way; and not textually. The library is inspired by Statecharts; Sequential Function Charts; Safe State Machines (SSM) and Mode-Automata. It has been designed so that only small extensions to Modelica 3.1 are needed. The algorithms are sketched that are used to guarantee consistent graphs that give a limited number of event iterations. Furthermore; it is shown how a symbolic verifier can be used to guarantee additional properties of state machines.


ModeGraph; Statechart; Sequential Function Charts; Mode-Automata; Safe State Machines; NuSMV; reactive systems; hybrid systems


André; C. (2003): Semantics of S.S.M (Safe State Machine). I3S Laboratory – UMR 6070 University of Nice-Sophia Antipolis / CNRS. Www.i3s.unice.fr/~map/WEBSPORTS/Documents/2003a2005/SSMsemantics.pdf

Bauschat; M.; Mönnich; W.; Willemsen; D.; and Looye; G. (2001): Flight testing Robust Autoland Control Laws. In Proceedings of the AIAA Guidance; Navigation and Control Conference; Montreal CA.

Benveniste A.; Caspi P.; Edwards S.A.; Halbwachs N.; Le Guernic P.; and Simone R. (2003): The Synchronous Languages Twelve Years Later. Proc. Of the IEEE; Vol.; 91; No. 1. Download: www.irisa.fr/distribcom/benveniste/pub/synch_ProcIEEE_2002.pdf

Dressler I. (2004): Code Generation From Jgrafchart to Modelica. Master thesis. Supervisor: Karl-Erik Arzen; Department of Automatic Control; Lund Institute of Technology; Lund; Sweden. Www.control.lth.se/documents/2004/5726.pdf

Dymola (2009). Dymola Version 7.3. Dassault Systèmes; Lund; Sweden (Dynasim). Www.dymola.com/.

Elmqvist H.; Otter. M.; Henriksson D.; Thiele B.; Mattssson; S.E. (2009): Modelica for Embedded Systems. In Proc. Of Modelica’2009 Conference; Como; Italy. Www.modelica.org/events/modelica2009

Franke R.; Casella F.; Otter M.; Proelss K.; Sieleman M.; Wetter M. (2009): Standardization of thermo-fluid modeling in Modelica.Fluid 1.0. In Proc. Of Modelica’ 2009 Conference; Como; Italy. Www.modelica.org/events/modelica2009

Harel; D. (1987): Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8; 231-274. Department of Applied Mathematics; The Weizmann Institute of Science; Rehovot; Israel. Www.inf.ed.ac.uk/teaching/courses/seoc1/-2005_2006/resources/statecharts.pdf

Lynch N.; Segala R.; and Vaandrager F. (2002): Hybrid I/O Automata. MIT Laboratory for Computer Science; techreport; MIT-LCS-TR-827b. Download: theory.lcs.mit.edu/tds/papers/Lynch/HIOA-final.ps

Malmheden M.; Elmqvist H.; Mattsson S.E.; Henriksson D.; and Otter M. (2008): ModeGraph - A Modelica Library for Embedded Control Based on Mode-Automata. B. Bachmann (editor); in Proc. Of Modelica’ 2008 conference; Bielefeld; Germany. Www.modelica.org/events/modelica2008/Proceedings/sessions/session3a3.pdf

Maraninchi; F. and Rémond; Y. (2002): Mode-Automata: a New Domain-Specific Construct for the Development of Safe Critical Systems. Www-verimag.imag.fr/~maraninx/SCP2002.html

Modelica (2009). Modelica Language Specification 3.1. www.modelica.org/documents/ModelicaSpec31.pdf

Mosterman P.J.; Otter M.; and Elmqvist H. (1998): Modeling Petri Nets as Local Constraint Equations for Hybrid Systems Using Modelica. In Proceedings of SCS Summer Simulation Conference; pp. 314-319; Reno; Nevada; July. Www.modelica.org/publications/papers/scsc98fp.pdf

NuSMV (2009): A symbolic model checker. Nusmv.irst.itc.it.

Otter; M.; Årzén; K.-E.; Dressler; I. (2005): StateGraph - A Modelica Library for Hierarchical State Machines. Proceedings of the 4th International Modelica Conference. TU-Hamburg-Harburg; Germany. Www.modelica.org/events/Conference2005/online_proceedings/Session7/Session7b2.pdfStateflow (2009): www.mathworks.com/products/stateflow

Citeringar i Crossref