The Fundamentals of Hybrid Systems Modelers Albert Benveniste INRIA Rennes

Albert Benveniste

Description

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.

• standard analysis


• considered hybrid system


• facto standard


• structure over


• clock configurations


• any infinite


• condition y0


• variables x˙

Sujets

• Robinson
• Caillaud
• Benveniste
• Analysis
• maths
• Mathématiques

Informations

• Publié par: pefav
• Nombre de lectures: 16
• Langue: English

Extrait

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 • 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. I NTRODUCTION map. (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- 2 at run time[18]. opment, for computer controlled systems. Simulinkhas be- come the de facto standard for physical system modeling and To reconcile requirements (a)–(c), we first propose using simulation. Noticeably, by building on top of the success of non standard analysisas a semantic domain for hybrid Simulink, TheMathworks was able to take over the market of systems. Second, we develop a comprehensiveconstructive embedded systems design, for many sectors. This speaks for semanticsfor hybrid systems. — the constructive semantics itself regarding the importance of such tools. In this paper we was first proposed by G. Berry [7] as a mathematical theory focus on general modelers, aimed at modeling and simulation on 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 S IMPLE H YBRID . Section IV is the core 3 Scicos isa freeware developed by Ramine Nikoukhah at of 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 model Related work is analysed in section V. More results can be complex multi-physics systems. In Modelica, equations have found in the extended version of this paper [2]. no pre-defined causality. Hybrid systems modelers raise a II. B ACKGROUND ON NON - STANDARD ANALYSIS number of difficult issues: • The key difficulty in reconciling requirements (a)–(c) is Since simulations use a single, global, solver, the choice and tuning of the integration method is global to the to give proper semantics to the inherently continuous time system. This may cause undesirable interactions between statement: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 + ,(y t+∂ −y t ) =x t , where expression “∂'0” is a ∂ a combination of complex operations whose scheduling non-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. 2 in 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