Towards Automatic Generation of Model Checkable Code From Modelica
Håkan Lundvall, Peter Bunus, Peter Fritzson · 2004
Using model components in complex system modeling is sometimes difficult because many semantic properties that should be obeyed during the design are not formalized in the modeling language. There exist rules that users of the components should follow in order to create semantically, mathematically, and physically correct models. Program verification aims at proving that programs meet certain specifications, i.e. that the actual program behavior fulfils certain specified properties. Model checking is a specific approach to verification of temporal properties of reactive and concurrent systems. Verification is usually carried out by using model checking algorithms to demonstrate the satisfiability of certain properties formalized as logical formulae over the model of the system. The model checking approach has proven successful for models based on finite-state automata and is based on state space inspection. To realize the full potential of the simulated and modeled systems with Modelica it is important to verify important properties of models in order to ensure that they meet the required criteria. In this paper we describe an algorithm that translates a non-trivial subset of Modelica to the model checking language of HyTech.