Hybrid CC, Hybrid Automata and Program Verification
Vineet Gupta, Radha Jagadeesan, Vijay Saraswat
Synopsis
We demonstrate the relationship of Hybrid CC to the methodology and
tools developed in the research on verification of hybrid systems ---
for example, see earlier proceedings of this conference for a variety
of approaches and tools.
We aim to establish
Hybrid CC as a high-level programming notation for hybrid automata ---
much as synchronous programming languages are high level notation for
discrete automata. Concretely, we establish the expressiveness of Hybrid CC
in two ways:
-
-
For any given hybrid automaton, we describe a Hybrid CC program whose
only traces are valid runs of the system.
- For any given safety property expressed in (real-time) temporal
logic, we show how to write a Hybrid CC program that "detects" if the
property is violated.
Furthermore, we aim to make programs written in
Hybrid CC amenable to the tools developed for the verification of hybrid
systems. For any Hybrid CC program, we build an automaton whose valid
runs are precisely execution traces of the program.
Postscript file.