Relating Hybrid Chi to Other Formalisms

Abstract

The hybrid χ (Chi) formalism is suited to modeling, simulation and verification of hybrid systems. It integrates concepts from dynamics and control theory with concepts from computer science, in particular from process algebra and hybrid automata. In this paper, we first provide an overview of χ. Then, the χ formalism is related to other formalisms by means of translation schemes: a translation scheme from continuous-time PWA systems to χ, a translation scheme from discrete-time PWA systems to χ, and a translation scheme from hybrid automata to χ. In order to be able to use existing model checkers that use hybrid automata like input languages, we developed and implemented a translation scheme from a subset of χ to hybrid automata. To illustrate this approach, a case study has been performed: a water level monitor has been modeled using χ. Using the implemented translation scheme from χ to hybrid automata, we obtain a hybrid automata model for the water level monitor. From this model, code that can be used as input for the model checker PHAVer is generated. © 2007 Elsevier B.V. All rights reserved.