Hybrid CC, Hybrid Automata and Program Verification

Vineet Gupta, Radha Jagadeesan, Vijay Saraswat


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.

© Springer Verlag, 2002. Published in the Lecture Notes in Computer Science Series.

  author =       "Vineet Gupta and Radha Jagadeesan and Vijay Saraswat",
  title =        "Hybrid cc, hybrid automata, and program verification",
  booktitle =    " Hybrid Systems III ",
  editor=        "Alur and Henzinger and Sontag",
  series =       "Lecture Notes in Computer Science",
  volume =       "1066",
  pages =        "52--63",
  year =         "1996",
  publisher=     "Springer Verlag"
Postscript file (193K)
Pdf file (134K)