From Simulation Models to Hybrid Automata Using Urgency and Relaxation
Stefano Minopoli, Goran Frehse · 2016
We consider the problem of translating a deterministic \emph{simulation model} (like Matlab-Simunk, Modelica or Ptolemy models) into a \emph{verification model} expressed by a network of hybrid automata. The goal is to verify safety using reachability analysis on the verification model. Simulation models typically use transitions with urgent semantics, which must be taken as soon as possible. Urgent transitions also make it possible to decompose systems that would otherwise need to be modeled with a monolithic hybrid automaton.