|
|
On Modelling and Reasoning about Hybrid SystemsThis paper concerns the development of formal approaches for specification, simulation
and validation of real-time reactive systems. Most previous approaches to this problem
have focussed on discrete systems wherein the behavior of the system is described
as a sequence of discrete events or state changes; they do not provide a satisfactory
solution for a wide range of hybrid systems whose behavior depends on discrete as
well as continuous parameters. Several approaches have been proposed to model such hybrid
systems, but they are not amenable to efficient simulation. We also show that these
approaches cannot conveniently express a variety of triggering and preemption policies. We
then present our approach to overcoming these problems, based on our model TRACE(H). Our
approach is aimed at retaining the (relative) simplicity of discrete systems as far as
possible, while still permitting descriptions of continuous behavior. Moreover, our
approach can express many different triggering, enabling and preemption policies so as to
conveniently model diverse hybrid systems. We also illustrate how simulation and
mechanical reasoning can be accomplished for systems represented in TRACE(H). Trade-offs
between expressive power and computational complexity are also discussed. |
|
Maintained by Sekar, sekar@cs.sunysb.edu |