The Fundamentals of Hybrid Systems Modelers Albert Benveniste INRIA Rennes
6
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe et accède à tout notre catalogue !
Découvre YouScribe et accède à tout notre catalogue !
6
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
The Fundamentals of Hybrid Systems Modelers Albert Benveniste, INRIA-Rennes Campus de Beaulieu 35042 Rennes cedex, France Benoît Caillaud, INRIA-Rennes Campus de Beaulieu 35042 Rennes cedex, France Marc Pouzet, LIENS École normale supérieure 45 rue d'Ulm 75230 Paris Cedex 05, France Abstract—Hybrid systems modelers have become the corner stone of embedded system development, with Simulink a de facto standard and Modelica a new player. Such tools still raise a number of issues that, we believe, require more fundamental understanding. In this paper we propose using non standard analysis as a semantic domain for hybrid systems — non standard analysis is an extension of classical analysis in which infinitesimals (the ? and ? in the celebrated generic sentence ???? . . . in college maths) can be manipulated as first class citizens. This allows us to provide a denotational semantics and a constructive semantics for hybrid systems, thus establishing simulation engines on a firm mathematical basis. In passing, we cleanly separate the job of the numerical analyst (solving differ- ential equations) from that of the computer scientist (generating execution schemes).1 I. INTRODUCTION Hybrid systems modelers have become in the last two decades the corner stone of complex embedded system devel- opment, for computer controlled systems. Simulink2 has be- come the de facto standard for physical system modeling and simulation. Noticeably, by building on top of the success of Simulink, The Mathworks was able to take over the market of embedded systems design, for many sectors.
Voir
- standard analysis
- considered hybrid system
- facto standard
- structure over
- clock configurations
- any infinite
- condition y0
- variables x˙
Publié par
Langue
English
The Fundamentals of Hybrid Systems Modelers
Albert Benveniste, INRIA-Rennes Campus de Beaulieu 35042 Rennes cedex, France
Benot Caillaud, INRIA-Rennes Campus de Beaulieu 35042 Rennes cedex, France
Marc Pouzet, LIENS Ècole normale suprieure 45 rue d’Ulm 75230 Paris Cedex 05, France
Abstract—Hybrid systems modelers have become the corner•How discrete is the semantics of the discrete part of a stone of embedded system development, with Simulink a de facto hybrid system modeler? Often, discrete and continuous standard and Modelica a new player. Such tools still raise a are not cleanly separated [2]. number of issues that, we believe, require more fundamental •What are the consequences for compilation of Modelica’s understanding. In this paper we propose usingnon standard “acausal” approach? analysisas a semantic domain for hybrid systems — non standard analysis is an extension of classical analysis in which Overall, we think that, with the exception of [18], no funda-infinitesimals (theεandηin the celebrated generic sentence mental answer has been provided to the difficulty raised by ∀ε∃η . . .in college maths) can be manipulated as first class the following justified although contradictory requirements: citizens. This allows us to provide a denotational semantics and a constructive semantics for hybrid systems, thus establishing (a) Thesemantic function, mapping a hybrid systems spec-simulation engines on a firm mathematical basis. In passing, we ification to its executable mathematical model (its oper-cleanly separate the job of the numerical analyst (solving differ-ational semantics), should bestaticallydefineable. ential equations) from that of the computer scientist (generating (b) Computers can only run according to discrete steps, 1 execution schemes). hence discretizing must be part of defining the semantic I. INTRODUCTIONmap. (c) Toachieve high computational quality with high flexibil-Hybrid systems modelers have become in the last two ity, the discretization scheme must be fixed adaptively, decades the corner stone of complex embedded system devel-2at run time[18]. opment, for computer controlled systems. Simulinkhas be-come the de facto standard for physical system modeling andTo reconcile requirements (a)–(c), we first propose using simulation. Noticeably, by building on top of the success ofnon standard analysisas a semantic domain for hybrid Simulink, TheMathworks was able to take over the market ofsystems. Second, we develop a comprehensiveconstructive embedded systems design, for many sectors. This speaks forsemanticsfor hybrid systems. — the constructive semantics itself regarding the importance of such tools. In this paper wewas first proposed by G. Berry [7] as a mathematical theory focus on general modelers, aimed at modeling and simulationon which to build synchronous languages’ compilers. of any type of hybrid system and we refer the reader to [10]The paper is organized as follows. Background on non for an overview of all tools related to hybrid systems analysis.standard analysis is provided in section II. Our mathematical Besides Simulink with its state-based extension Stateflow,formalism for hybrid systems specification is introduced in several such hybrid systems modelers have been developed.section III, we call it SIMPLEHYBRID. Section IV is the core 3 Scicos isa freeware developed by Ramine Nikoukhah atof our paper; a denotational semantics is given based on non 4 INRIA [19], [17]. Modelicais a non-proprietary, object-standard analysis; then, a constructive semantics is provided. oriented, equation based language to conveniently modelRelated work is analysed in section V. More results can be complex multi-physics systems. In Modelica, equations havefound in the extended version of this paper [2]. no pre-defined causality. Hybrid systems modelers raise a II. BACKGROUND ON NON-STANDARD ANALYSIS number of difficult issues: •The key difficulty in reconciling requirements (a)–(c) isSince simulations use a single, global, solver, the choice and tuning of the integration method is global to theto give proper semantics to the inherently continuous time system. This may cause undesirable interactions betweenstatement:y˙ =x. In non-standard analysis, this statement sub-systems that seemingly should not interact [2].means,by definition of the derivative of a function:∀∂'0, 1 •Zero-crossings,which trigger mode changes, can involve∀t∈R+,(yt+∂−yt) =xt, where expression “∂'0” is a ∂ a combination of complex operations whose schedulingnon-standardexpression that reads:“∂is infinitesimal”. may be delicate.Non-standard analysis has been proposed by Abraham Robinson in the 60’s to allow handling explicitly “infinitesi-1 This work was supported by the INRIA “Action d’envergure” mals” in analysis [1], [16]. Robinson’s approach is axiomatic, SYNCHRONICS. 2in that he proposes enriching the basic ZFC (Zermelo-http://www.mathworks.com/products/simulink/ Fraenkel) framework with three more axioms. There has 3 http://www-rocq.inria.fr/scicos/ 4 http://www.modelica.org/been much debate in the community of mathematicians as to
