Verification tools for linear hybrid automata
Goran Frehse · Cambridge University Press eBooks · 2009
Linear hybrid automata are of interest in verification because sets of successor states can be computed exactly and efficiently using integer arithmetic. This fact is exploited in a number of formal verification algorithms that upon termination give a mathematically sound answer on whether a property holds or not. This chapter gives an overview of verification algorithms for safety properties of linear hybrid automata, and some of the over-approximation techniques that help to make the tools applicable in practice . Formal verification and linear hybrid automata Formal verification tries to establish with absolute certainty, in the sense of being mathematically provable, whether or not a given property is satisfied or violated by a system. In this chapter we consider algorithmic approaches to verification of safety properties such as whether a set of forbidden states is reachable. If a verification algorithm is exact (no over-approximations, no floating point computations, no rounding of any kind, etc.) and terminates, it gives the provably correct answer: safe or unsafe. Exact verification algorithms are of limited use for hybrid systems in general, since the solution of a differential equation can only be computed up to some accuracy. One may have to resort to an over-approximative algorithm, i.e. use over-approximations in the sense that when the algorithm terminates with result safe , the system really is safe. If the algorithm finds a violation, one might not know whether the violation is real or an artifact of over-approximations.