Hybrid CC, Hybrid Automata and Program Verification

Synopsis

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.

@InProceedings{hcc-automata,
  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"
}