Parameter Synthesis for Hybrid Automata

This chapter talks about the inverse 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. As for purely timed systems, it is handy when verifying hybrid systems to use parameters either to describe uncertainties or to introduce tuning parameters that are subject to optimization. Instead of setting these parameters manually and then verifying the resulting concrete system, parameterized models are used to perform automatic parameter synthesis. The chapter first talks about algorithms for hybrid automata. The presented algorithms have been implemented in HyMITATOR, an extension of IMITATOR for hybrid automata. It presents a running example, a distributed temperature control system to illustrate the presented concepts. The chapter is mainly based on Fribourg and Kühne's work.