Model-based Engineering of Embedded Systems Using the Hybrid Process Algebra Chi
J. C. M. Baeten, D.A. van Beek, Pjl Pieter Cuijpers, Michel A. Reniers, J.E. Rooda, Ramon R. H. Schiffelers, R.J.M. Theunissen · Electronic Notes in Theoretical Computer Science · 2008
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.