Search

Abstract: Hybrid Chi is a process algebra for the modeling and analysis of hybrid systems. It enables modular specification of hybrid systems by means of a large set of atomic statements and operators for combining these. For the efficient implementation of simulators and the verification of properties of hybrid systems it is convenient to have a model that uses a more restricted part of the syntax of hybrid Chi. To that purpose the linearization of a reasonably expressive, relevant subset of the Chi language is discussed. A linearization algorithm that transforms any specification from this subset into a so-called normal form is presented. The algorithm is applied to a bottle-filling line example to demonstrate tool-based verification of Chi models. [Copyright &y& Elsevier]

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. [Copyright &y& Elsevier]