Hybrid system modelers have become a corner stone of complex embedded system development. Embedded systems include not only control components and software, but also physical devices. In this area, Simulink is a de facto standard design framework, and Modelica
a new player. However, such tools raise several issues related to the lack of reproducibility of simulations (sensitivity to simulation parameters and to the choice of a simulation engine). In this paper we propose using techniques from non-standard analysis to define a semantic domain for hybrid systems. Non-standard analysis is an extension of classical analysis in which infinitesimal (the "epsilon" and "eta" in the celebrated generic sentence "for all epsilon there exists eta..." of college maths) can be manipulated as first class citizens. This approach allows us to define both a denotational semantics, a constructive semantics, and a Kahn Process Network semantics for hybrid systems, thus establishing simulation engines on a sound but flexible mathematical foundation. These semantics offer a clear distinction
between the concerns of the numerical analyst (solving differential equations) and those of the computer scientist (generating execution schemes). We also discuss a number of practical and fundamental issues in hybrid system modelers that give rise to non reproducibility of
results, nondeterminism, and undesirable side effects. Of particular importance are cascaded mode changes (also called ``zero-crossings'' in the context of hybrid systems modelers).

Keywords : hybrid systems, hybrid systems modelers, modeling, non-standard analysis

pdf

link to reprint

Nota: We have been kindly made aware by Dino Mandrioli of the following missing reference in our work:

Heinrich Rust
Operational Semantics for Timed Systems: A Non-standard Approach to Uniform Modeling of Timed and Hybrid Systems
Lecture Notes in Computer Science, Springer, Volume 3456, 2005, DOI: 10.1007/b135629

This is a very relevant reference. Although different topics are adressed regarding hybrid systems, this book deals with hybrid systems and in particular hybrid automata. Non-standard analysis is used in its axiomatic form.

Also, Dino Mandrioli himself, jointly with Angelo Gargantini and Angelo Morzenti, have used non-standard analysis is a quite different context, namely for the axiomatic study of zero-time transitions in timed systems, with an illustration on Petri nets. Again, non-standard analysis is used in its axiomatic form. The reference is:

Angelo Gargantini, Dino Mandrioli, Angelo Morzenti: Dealing with Zero-Time Transitions in Axiom Systems. Inf. Comput. 150(2): 119-131 (1999)