Survey on hybrid verification

OData support
Vörös András
Department of Measurement and Information Systems

Nowadays safety critical systems are becoming increasingly prevalent, however, faults in their behaviour can lead to serious damage. Therefore, it is extremely important to use mathematically precise verification techniques to prove their correctness.

Most safety critical systems are hybrid systems - that is, they contain both continuous and discrete components which results in incredibly complex behaviours. To formally verify these systems, their behaviour is modelled by a high level state-based formalism, called the hybrid automaton that describes discrete behaviour similarly to the conventional finite automaton, and describes continuous behaviour using differential equations.

This formalism makes it easy to describe hybrid systems, however in order to successfully prove the correctness of such systems, efficient verification techniques are desired. Verification of purely discrete or purely continuous systems are already complex tasks, but combining the two types of behaviours makes the problem generally algorithmically undecidable.

However, verification of such systems is an inevitable task and many tools and approaches exist with this goal. To overcome the complexity these tools often work on just a subset of hybrid automata, or a modification of verification problems. It is also common to use approximations during calculations (that may result in incorrect answers).

In my work I compare the most important algorithms and tools available for modelling and verification of hybrid automata, considering the supported types of hybrid automata and their effectiveness. In order to do so I have designed a software that provides a common platform for modelling hybrid automata and makes verification possible by supporting multiple existing tools for hybrid verification. This way I can compare the tools by executing them on the same inputs.


Please sign in to download the files of this thesis.