Extending model checkers for hybrid system verification: the case study of SPIN.

Abstract

A hybrid system is a system that evolves following a continuous dynamic, which may instantaneously change when certain internal or external events occur. Due to this combination of discrete and continuous dynamics, the behavior of a hybrid system is, in general, difficult to model and analyze. Model checking techniques have been proven to be an excellent approach to analyze critical properties of complex systems. This paper presents a new methodology to extend explicit model checkers for hybrid systems analysis. The explicit model checker is integrated, in a non-intrusive way, with some external structures and existing abstraction libraries, which store and manipulate the abstraction of the continuous behavior irrespective of the underlying model checker. The methodology is applied to SPIN using Parma Polyhedra Library. In addition, the authors are currently working on the extension of other model checkers.