Resumen:
Hybrid systems are characterized by combining discrete and continuous behaviors. Verification of hybrid systems is, in general, a difficult task due to the potential complexity of the continuous dynamics. Currently, there are different formalisms and tools which are able to analyze specific types of hybrid systems, model checking being one of the most used approaches. In this paper, we propose an extension of the discrete model checker Java Path Finder in order to analyze hybrid systems. We apply a general methodology which has been successfully used to extend SPIN. This methodology is non-intrusive, and uses external libraries, such as Parma Polyhedra Library, to abstract the continuous behavior of the hybrid system independent to the underlying model checker.