From synchronous programs to symbolic representations of hybrid systems

In this paper, we present an extension of the synchronous language Quartz by new kinds of variables, actions and statements for modeling the interaction of synchronous systems with their continuous environment. We present an operational semantics of the obtained hybrid modeling language and moreover show how compilation algorithms that have been originally developed for synchronous languages can be extended to these hybrid programs. Thus, we can automatically translate the hybrid programs to compact symbolic representations of hybrid transition systems that can be immediately used for simulation and formal verification. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; F.3.1 [Theory of Computation]: Specifying and Verifying and Reasoning about Programs; F.3.2 [Theory of Computation]: Semantics of Programming Languages General Terms Languages, Verification. Keywords Hybrid Systems, Synchronous Languages, Symbolic Representation of Trans...

• Type: Conference
• Year: 2010
• Where: HYBRID
• Authors: Kerstin Bauer, Klaus Schneider
• Keywords: HYBRID 2010, Hybrid Programs, Hybrid Systems, Synchronous Language Quartz, Synchronous Languages