A New Formalism for Modeling of Reactive and Hybrid Systems

Martin Otter, Martin Malmheden, Hilding Elmqvist, Sven-Erik Mattsson, Charlotta Johnsson

Research output: Chapter in Book/Report/Conference proceedingPaper in conference proceedingpeer-review


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 for simple usage, to guarantee safety properties and to harmonise 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.
Original languageEnglish
Title of host publication[Host publication title missing]
Number of pages14
Publication statusPublished - 2009
Event7th International Modelica Conference, 2009 - Como, Italy
Duration: 2009 Sep 202009 Sep 22
Conference number: 7


Conference7th International Modelica Conference, 2009

Subject classification (UKÄ)

  • Control Engineering


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


Dive into the research topics of 'A New Formalism for Modeling of Reactive and Hybrid Systems'. Together they form a unique fingerprint.

Cite this