TY - JOUR
T1 - Relating Hybrid Chi to Other Formalisms
AU - van Beek, D. A.
AU - Rooda, J. E.
AU - Schiffelers, R. R.H.
AU - Man, K. L.
AU - Reniers, M. A.
PY - 2007/10/6
Y1 - 2007/10/6
N2 - 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.
AB - 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.
KW - PWA systems
KW - hybrid automata
KW - hybrid systems
KW - modelling
KW - simulation
KW - verification
UR - http://www.scopus.com/inward/record.url?scp=34848817792&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2006.09.041
DO - 10.1016/j.entcs.2006.09.041
M3 - Article
AN - SCOPUS:34848817792
SN - 1571-0661
VL - 191
SP - 85
EP - 113
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -