Hybrid Chi: A Process Algebra for Hybrid Systems

Ka Lok Man,  PhD Candidate at Formal Methods Group, Eindhoven University of Technology, The Netherlands
 

Abstract: Recently, the hybrid Chi formalism has been developed. The hybrid Chi formalism is suited to modeling, simulation and verification of hybrid systems. The semantics of hybrid Chi is defined by means of deduction rules (in SOS style) that associate a hybrid transition system with a hybrid Chi process. A set of axioms is presented for a notion of bisimilarity. The hybrid Chi formalism integrates concepts from dynamics and control theory with concepts from computer science, in particular from process algebra and hybrid automata. It integrates ease of modeling with straightforward semantics. Its `consistent equation semantics' enforces state changes to be consistent with delay predicates that combine the invariant and flow clauses of hybrid automata. Ease of modeling is ensured by means of the following concepts: 1) different classes of variables: discrete and continuous, of subclass jumping or non-jumping, and algebraic; 2) strong time determinism of alternative composition in combination with delayable guards; 3) integration of urgent and non-urgent actions; 4) differential algebraic equations as a process term as in mathematics; 5) steady-state initialization; and 6) several user-friendly syntactic extensions. Furthermore, the hybrid Chi formalism incorporates several concepts for complex system specification: 1) process terms for scoping that integrate abstraction, local variables, local channels and local recursion definitions; 2) process definition and instantiation that enable process re-use, encapsulation, hierarchical and/or modular composition of processes; and 3) different interaction mechanisms: handshake synchronization and synchronous communication that allow interaction between processes without sharing variables, and shared variables that enable modular composition of continuous time or hybrid processes.

The possibility of developing efficient algorithms for the linearization of hybrid Chi processes has been investigated. Furthermore, a formal translation of a subset of hybrid Chi to hybrid automata and vice versa has been defined. It is proved that any transition of a hybrid Chi model can be mimicked by a transition in the corresponding hybrid automaton model and vice versa, which indicates that the translation as defined is correct. The translation from hybrid Chi to hybrid automata enables verification of hybrid Chi models using existing hybrid automata based verification tools.

For the purpose of simulation and verification of hybrid Chi models, tools have been developed. The Stepper tool generates generalized transitions. Based on this Stepper, two simulators have been developed: a symbolic simulator, and a numeric simulator based on the Simulink S-function interface. Finally, the translation from hybrid Chi to hybrid automata has been automated.


About the speaker: Ka Lok Man was born in Hong Kong, China, in 1969. He holds a Dr. Eng. degree in Electronic Engineering from Politecnico di Torino, Turin, Italy.

He was with Idem and Fiat Auto (Turin, Italy) from 1997 to 1999. From June 1999 through September 2000, he was a research assistant at the Electronic Design Automation Group, Dep. of Electrical and Computer Engineering, Politecnico di Torino.

Between September 1999 and August 2000, he was also a visiting researcher at the VLSI/CAD Group, Dep. Of Electrical and Computer Engineering, University of Colorado at Boulder, USA. He was with STMicroelectronics (Agrate, Milan, Italy) from 2000 to 2002. Since then, he has been with the Formal Methods Group, Dep. of Computer Science, Eindhoven University of Technology, the Netherlands, where he is currently a Ph.D. student.

His research interests include formal verification of digital integrated circuits and systems, SystemC codesign, process algebras, formal analysis of real-time and hybrid systems.


Download visuals (488 kB pdf)