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|
Baeten, J. C. M., Beek, van, D. A., Cuijpers, P. J. L., Reniers, M. A., Rooda, J. E., Schiffelers, R. R. H., & Theunissen, R. J. M. (2008). Model-based engineering of embedded systems using the hybrid process algebra Chi. In C. Palamidessi, & F. D. Valencia (Eds.), Proceedings LIX Colloquium on Emerging Trends in Concurrency Theory (Paris, France, November 13-15, 2006) (pp. 21-53). (Electronic Notes in Theoretical Computer Science; Vol. 209). https://doi.org/10.1016/j.entcs.2008.04.003