The Inverse Method: Parametric Verification of Real-time Embedded Systems

5

Parameter Synthesis for Hybrid Automata

We introduced in Chapter 2 the inverse method for timed automata. Here, we extend this method to a larger class of systems, namely hybrid systems. This class of systems involves continuous variables, which are real-valued variables that can have an arbitrary dynamics. Hybrid systems combine continuous and discrete behavior. They are especially useful for the verification of embedded systems. Indeed, they allow the unified modeling of the interaction of a discrete control with a continuous environment, that involves system variables such as position, temperature or pressure.

There are several classes of formal models for hybrid systems. In general, there is a trade-off between the expressivness of the model and the complexity of the algorithmic apparatus that is needed for its formal analysis. Linear hybrid automata provide a good compromise. In contrast to more general hybrid automata models, which allow arbitrary dynamics of the continuous state variables, linear hybrid automata are restricted to linear dynamics. This allows the use of efficient algorithms based on convex polyhedra. Furthermore, more complex dynamics – like hybrid automata with affine dynamics – can easily be approximated conservatively by linear hybrid automata. Although reachability is undecidable for linear hybrid automata [HEN 98], practically relevant results have been obtained using this formalism [HEN 97]. Timed automata can be seen as a subclass of hybrid automata, ...