Hybrid Automata for Formal Modeling and Verification of Cyber-Physical Systems.
S. N. Krishna and Ashutosh Trivedi
The presence of a tight integration between the discrete control
(the "cyber") and the analog environment (the "physical")-via sensors and
actuators over wired or wireless communication networks-is the defining
feature of cyber-physical systems. Hence, the functional correctness of a
cyber-physical system is crucially dependent not only on the dynamics of
the analog physical environment, but also on the decisions taken by the
discrete control that alter the dynamics of the environment. The framework
of Hybrid automata--introduced by Alur, Courcoubetis, Henzinger, and
Ho--provides a formal modeling and specification environment to analyze
the interaction between the discrete and the continuous parts of cyber-physical
systems. Hybrid automata can be considered as generalizations
of finite state automata augmented with a finite set of real-valued variables
whose dynamics in each state is governed by a system of ordinary differential
equations. Moreover, the discrete transitions of hybrid automata
are guarded by constraints over the values of these real-valued variables,
and enable discontinuous jumps in the evolution of these variables. Considering
the richness of the dynamics in a hybrid automaton, it is perhaps
not surprising that the fundamental verification questions, like reachability
and schedulability, for the general model are undecidable. In this article
we present a review of hybrid automata as modeling and verification
framework for cyber-physical systems, and survey some of the key results
related to practical verification questions related to hybrid automata.
Journal of the Indian Institute of Science, VOL 93:3, pages 419-440, Jul.-Sep. 2013.
PDF © 2013 IISc.