In this article, we present a model and a denotational semantics for hybrid systems. Our model is designed to be used for the verification of large, existing embedded applications. The discrete part is modeled by a program written in an extension of an imperative language and the continuous part is modeled by differential equations. We give a denotational semantics to the continuous system inspired by what is usually done for the semantics of computer programs and then we show how it merges into the semantics of the whole system. The semantics of the continuous system is computed as the fix-point of a modified Picard operator which increases the information content at each step. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Bouissou, O., & Martel, M. (2008). A hybrid denotational semantics for hybrid systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4960 LNCS, pp. 63–77). https://doi.org/10.1007/978-3-540-78739-6_5
Mendeley helps you to discover research relevant for your work.