Formal verification of Chi models using PHAVer

K.L. Man, R.R.H. Schiffelers

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

41 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationIFM 2005 Doctoral Symposium on Integrated Formal Methods (Eindhoven, The Netherlands, November 29, 2005)
EditorsJ.M.T. Romijn, G. Smith, J.C. Pol, van de
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Publication statusPublished - 2005

Publication series

NameComputer Science Reports
ISSN (Print)0926-4515


Dive into the research topics of 'Formal verification of Chi models using PHAVer'. Together they form a unique fingerprint.

Cite this