Formal verification of Chi models using PHAVer

The hybrid Chi (x) language is a formalism for modeling, simulation and verification of hybrid systems. One of the most widely known hybrid system formalisms is that of hybrid automata. The formal translation of x to hybrid automata enables verification of x specifications using existing hybrid automata based veri??cation tools. In this paper, we describe the translation from x to hybrid automata, and the relation between hybrid automata and the linear hybrid I/O automata that are used for the verification tool PHAVer (Polyhedral Hybrid Automaton Verifyer). In the case study, we translate a x specification to a linear hybrid I/O automaton, and use PHAVer to verify properties