Kalok Man

Formal Specification and Analysis of Hybrid Systems

Abstract:

The hybrid Chi formalism has been developed, and it 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 a straightforward semantics.

<p>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 (e.g. PHAVer and  HyTech).

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.

In this presentation, we first provide an overview of the current status of hybrid Chi,
and show some practical applications of hybrid Chi.
Then, we give an outline for the latest developments of hybrid Chi.