Relating Hybrid Chi to other formalisms

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)

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.
LanguageEnglish
Title of host publicationProceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) 29 November 2005, Eindhoven, The Netherlands
EditorsJ. Romijn, G. Smith, J. Pol, van de
Pages85-113
DOIs
StatePublished - 2007
Eventconference; Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) Eindhoven, The Netherlands; 2005-11-29; 2005-11-29 -
Duration: 29 Nov 200529 Nov 2005

Publication series

NameElectronic Notes in Theoretical Computer Science
Volume191
ISSN (Print)1571-0061

Conference

Conferenceconference; Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) Eindhoven, The Netherlands; 2005-11-29; 2005-11-29
Period29/11/0529/11/05
OtherDoctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) Eindhoven, The Netherlands

Fingerprint

Water levels
Continuous time systems
Hybrid systems
Control theory
Computer science
Algebra
Computer simulation

Cite this

Beek, van, D. A., Rooda, J. E., Schiffelers, R. R. H., Man, K. L., & Reniers, M. A. (2007). Relating Hybrid Chi to other formalisms. In J. Romijn, G. Smith, & J. Pol, van de (Eds.), Proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) 29 November 2005, Eindhoven, The Netherlands (pp. 85-113). (Electronic Notes in Theoretical Computer Science; Vol. 191). DOI: 10.1016/j.entcs.2006.09.041
Beek, van, D.A. ; Rooda, J.E. ; Schiffelers, R.R.H. ; Man, K.L. ; Reniers, M.A./ Relating Hybrid Chi to other formalisms. Proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) 29 November 2005, Eindhoven, The Netherlands. editor / J. Romijn ; G. Smith ; J. Pol, van de. 2007. pp. 85-113 (Electronic Notes in Theoretical Computer Science).
@inproceedings{9696ce3f2f094efc82c1b20bf072e52e,
title = "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.",
author = "{Beek, van}, D.A. and J.E. Rooda and R.R.H. Schiffelers and K.L. Man and M.A. Reniers",
year = "2007",
doi = "10.1016/j.entcs.2006.09.041",
language = "English",
series = "Electronic Notes in Theoretical Computer Science",
pages = "85--113",
editor = "J. Romijn and G. Smith and {Pol, van de}, J.",
booktitle = "Proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) 29 November 2005, Eindhoven, The Netherlands",

}

Beek, van, DA, Rooda, JE, Schiffelers, RRH, Man, KL & Reniers, MA 2007, Relating Hybrid Chi to other formalisms. in J Romijn, G Smith & J Pol, van de (eds), Proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) 29 November 2005, Eindhoven, The Netherlands. Electronic Notes in Theoretical Computer Science, vol. 191, pp. 85-113, conference; Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) Eindhoven, The Netherlands; 2005-11-29; 2005-11-29, 29/11/05. DOI: 10.1016/j.entcs.2006.09.041

Relating Hybrid Chi to other formalisms. / Beek, van, D.A.; Rooda, J.E.; Schiffelers, R.R.H.; Man, K.L.; Reniers, M.A.

Proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) 29 November 2005, Eindhoven, The Netherlands. ed. / J. Romijn; G. Smith; J. Pol, van de. 2007. p. 85-113 (Electronic Notes in Theoretical Computer Science; Vol. 191).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Relating Hybrid Chi to other formalisms

AU - Beek, van,D.A.

AU - Rooda,J.E.

AU - Schiffelers,R.R.H.

AU - Man,K.L.

AU - Reniers,M.A.

PY - 2007

Y1 - 2007

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.

U2 - 10.1016/j.entcs.2006.09.041

DO - 10.1016/j.entcs.2006.09.041

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 85

EP - 113

BT - Proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) 29 November 2005, Eindhoven, The Netherlands

ER -

Beek, van DA, Rooda JE, Schiffelers RRH, Man KL, Reniers MA. Relating Hybrid Chi to other formalisms. In Romijn J, Smith G, Pol, van de J, editors, Proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005) 29 November 2005, Eindhoven, The Netherlands. 2007. p. 85-113. (Electronic Notes in Theoretical Computer Science). Available from, DOI: 10.1016/j.entcs.2006.09.041