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.
|Title of host publication||Proceedings LIX Colloquium on Emerging Trends in Concurrency Theory (Paris, France, November 13-15, 2006)|
|Editors||C. Palamidessi, F.D. Valencia|
|Publication status||Published - 2008|
|Name||Electronic Notes in Theoretical Computer Science|