Model-based Engineering of Embedded Systems Using the Hybrid Process Algebra Chi

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.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Jos C. M. Baeten, Dirk A. van Beek, Pieter J. L. Cuijpers, Michel A. Reniers, J. E. Rooda, Ramon R. H. Schiffelers, Rolf J. M. Theunissen
• Keywords: ENTCS 2008, Hybrid Chi, Hybrid Systems, Process Algebra