A Hybrid Denotational Semantics for Hybrid Systems

11 years 1 months ago
A Hybrid Denotational Semantics for Hybrid Systems
Abstract. 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.
Olivier Bouissou, Matthieu Martel
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where ESOP
Authors Olivier Bouissou, Matthieu Martel
Comments (0)