Non-standard semantics of hybrid systems modelers

详细信息	查看全文 | 推荐本文 |

• 作者：Albert Benveniste^a ; ^{Albert.Benveniste@inria.fr} ; Timothy Bourke^a ; ^{Timothy.Bourke@inria.fr} ; Benoî ; t Caillaud^a ; ^{Benoit.Caillaud@inria.fr} ; Marc Pouzet^b ; ^{Marc.Pouzet@ens.fr}
• 关键词：Hybrid systems ; Hybrid systems modelers ; Non-standard analysis ; Non-standard semantics ; Constructive semantics ; Kahn process networks ; Compilation of hybrid systems
• 刊名：Journal of Computer and System Sciences
• 出版年：2012
• 期刊代码：186_00220000
• 类别：et
• 出版时间：May, 2012
• 卷：78
• 期：3
• 页码：877-910
• 文件大小：586 K

摘要

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 m>non-standard analysism> to define a semantic domain for hybrid systems. Non-standard analysis is an extension of classical analysis in which infinitesimal (the m>蔚m> and m>畏m> in the celebrated generic sentence 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, non-determinism, and undesirable side effects. Of particular importance are cascaded mode changes (also called 鈥渮ero-crossings鈥?in the context of hybrid systems modelers).