User Tools

Site Tools


Formal specification and analysis of hybrid systems

K.L. Man and R.R.H.Schiffelers

In this research, 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 Chi process. A set of axioms is presented for a notion of equivalence (bisimilation). 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 a 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: 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. In process algebra, linearization is a transformation of a recursive specification into a linear representation, i.e., a kind of normal form that is convenient for many forms of analysis. A first step towards the linearization of a reasonable subset of the hybrid Chi language has been carried out in the form of elimination theorems for a number of Chi operators. Furthermore, a formal translation of a subset of Chi to hybrid automata and vice versa has been defined. It is proved that any transition of a 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 Chi to hybrid automata enables verification of Chi models using existing hybrid automata based verification tools. For the purpose of simulation and verification of Chi models, tools have been developed. The stepper tool generates generalized transitions given a Chi process. Based on this stepper, a symbolic simulator has been developed. Finally, the translation from Chi to hybrid automata has been automated. The Chi formalism is illustrated by means of examples taken from several application domains. Case studies have been conducted to test the developed tools.

Ph.D. thesis, Eindhoven University of Technology, 2006.


vanbeek/phdmanschif.txt · Last modified: Wednesday, 19 March 2008 : 15:56:32 (external edit)