Formal verification of Chi models using PHAVer

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademic

29 Downloads (Pure)

Samenvatting

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.
Originele taal-2Engels
TitelIFM 2005 Doctoral Symposium on Integrated Formal Methods (Eindhoven, The Netherlands, November 29, 2005)
RedacteurenJ.M.T. Romijn, G. Smith, J.C. Pol, van de
Plaats van productieEindhoven
UitgeverijTechnische Universiteit Eindhoven
Pagina's39-48
StatusGepubliceerd - 2005

Publicatie series

NaamComputer Science Reports
Volume05-29
ISSN van geprinte versie0926-4515

Vingerafdruk Duik in de onderzoeksthema's van 'Formal verification of Chi models using PHAVer'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    Man, K. L., & Schiffelers, R. R. H. (2005). Formal verification of Chi models using PHAVer. In J. M. T. Romijn, G. Smith, & J. C. Pol, van de (editors), IFM 2005 Doctoral Symposium on Integrated Formal Methods (Eindhoven, The Netherlands, November 29, 2005) (blz. 39-48). (Computer Science Reports; Vol. 05-29). Technische Universiteit Eindhoven.