Conference article

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

Download article

Published in: Proceedings of the 7th International Modelica Conference; Como; Italy; 20-22 September 2009

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

Show more +

Published: 2009-12-29

ISBN: 978-91-7393-513-5

ISSN: 1650-3686 (print), 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.

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:

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.

Dymola (2009). Dymola Version 7.3. Dassault Systèmes; Lund; Sweden (Dynasim).

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

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.

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.

Lynch N.; Segala R.; and Vaandrager F. (2002): Hybrid I/O Automata. MIT Laboratory for Computer Science; techreport; MIT-LCS-TR-827b. Download:

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.

Maraninchi; F. and Rémond; Y. (2002): Mode-Automata: a New Domain-Specific Construct for the Development of Safe Critical Systems.

Modelica (2009). Modelica Language Specification 3.1.

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.

NuSMV (2009): A symbolic model checker.

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. (2009):

Citations in Crossref