A New Formalism for Modeling of Reactive and Hybrid Systems

Abstract

A new Modelica library is presented that is used to model safe hierarchical state machines in combina- tion with any Modelica model, e.g., controllers, logi- cal blocks, and physical systems described by diffe- rential-algebraic equations. It has been designed to simplify usage, improve safety aspects and to har- monize with the design of the new Modeli- ca_EmbeddedSystems library. Furthermore, new blocks are introduced to define actions in a visual way, and not textually. The library is inspired by Sta- techarts, Sequential Function Charts, Safe State Ma- chines (SSM) and Mode-Automata. It has been de- signed 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 li- mited number of event iterations. Furthermore, it is shown how a symbolic verifier can be used to guar- antee additional properties of state machines