A Hybrid Denotational Semantics for Hybrid Systems -- Extended Version

27 pagesIn this article, we present a model and a denotational semantics for hybrid systems made of a continuous and a discrete subsystem. Our model is designed so that it may be easily used for modeling large, existing, critical embedded applications, which is a first step toward their validation. The discrete subsystem is modeled by a program written in an extension of an imperative language and the continuous subsystem is modeled by differential equations. We give to both subsystems a denotational semantics inspired by what is usually done for the semantics of computer programs and then we show how the semantics of the whole system is deduced from the semantics of its two components. 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. This fix-point is computed as the supremum of a sequence of approximations and we show that this supremum exists and is the solution of a differential equation using Keye Martin's measurement theory. The semantics of the discrete system is given as a classical denotational semantics, except that special denotations are given for the actions of sensors and/or actuators