Accelerated Simulation of Hybrid Systems : Method combining static analysis and run-time execution analysis.

Ayman Aljarbouh 1
1 HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The theme of this dissertation is to deal with Zeno behaviour of hybrid systems from a simulation perspective. Hybrid systems can be defined as dynamical systems in which continuous and discrete dynamics interact with each other. Such systems exist in a large number of technological systems where the physical continuous evolution of the system is combined with embedded control actions. The mathematical models of hybrid systems consist typically of continuous time dynamics usually described by differential equations describing the continuous behaviour of the system, and discrete event dynamics such as finite state machines (synchronous or data-flow programs) that describe the discrete behaviour of the system. However, due to the complex interaction between the continuous and discrete dynamics, designers should pay special attention when modelling hybrid systems. In fact, realistic models of hybrid systems almost always necessitate part of the hybrid system’s physical behaviour to be abstracted by means of “ideal equations” such as reset and conditional constraints that typically lead to discontinuities in physical signals. The term modelling abstraction is thus designated to any mechanism that enables concrete physical behaviour to be “hidden” by considering idealized models. Intuitively, because of such abstraction, the model jumps over instants corresponding to the violation of abstraction mechanisms. Such modelling abstraction mechanism may result in hybrid models that exhibit Zeno behaviour. Formally, we define Zeno behaviour as an infinite sequence of discrete events occurring in a finite amount of time. Basically, the presence of Zeno behaviour indicates that the hybrid system’s model incompletely describes the real physical behaviour of the system being modelled. If we consider the standard semantics of executions of hybrid systems models, the problem can best be described as follows: the physical system keeps evolving continuously beyond a certain point, but the model’s continuous evolution is undefined beyond that point, because of the infinity of the discrete transitions or mode switchings. Such inherent limitation of the hybrid system model makes the solution of the system reaches a (Zeno limit) point in time at which the model is no longer valid. This is due the fact that the modelling abstraction mechanism incompletely describes the complex interaction between the continuous and discrete dynamics of the hybrid system being modelled. That is, Zeno behaviour can be seen as a modelling artifact that can never occur in reality. Analytically, we distinguish between two different types of Zeno behaviour in hybrid systems: i) chattering-Zeno, and ii) genuinely-Zeno. In models that exhibit chattering- Zeno, the system infinitely moves back and forth between modes in a discrete fashion with infinitesimal time spent between the successive mode switchings. Any Zeno behaviour that is not chattering-Zeno can be classified as genuinely-Zeno. In this dissertation we focus on both chattering-Zeno and a particular type of genuinely-Zeno which we call geometric-Zeno. In models that exhibit geometric-Zeno, an accumulation of an infinite number of mode switchings occurs in finite time. Geometric-Zeno behaviour leads the solution of the system to converge to a Zeno limit point according to a geometric series. Roughly speaking, in geometric-Zeno models discrete events occur at an increasingly smaller distance in time, converging against a limit point. Zeno behaviour is highly challenging from a simulation perspective. In fact, although chattering-Zeno and geometric-Zeno are analytically different, the effect of these two types of Zeno during the numerical simulation is similar: the simulation process effectively stalls, halts and terminates with an error message, or becomes numerically incorrect and produces faulty results, as infinitely many discrete transitions would need to be simulated. This dissertation takes the perspective that models of hybrid systems are executable programs written in programming languages having a hybrid system semantics. Basically, defining a proper hybrid semantic model is the first step of developing a simulation framework for hybrid systems. This step is mandatory even before designing the language or the simulator. The development of a hybrid simulation framework typically include the following steps: 1. Properly define a hybrid semantic model that can account for the expected properties of the hybrid systems under simulation. 2. Design and develop a simulator that could approximate the model dynamics conforming to the defined hybrid semantic model. 3. Design a language capable of expressing all models elements and components conforming to the hybrid semantic model. Type-checking must be included in this step to prove statically the semantic validity of the simulated models. 4. Design a compiler for the language. The compiler should be capable of performing static checks of models and also rejecting models that are invalid. Many modelling and simulation tools for hybrid systems have been developed in the past years. They can be classified into two categories: those who put special attention on defining models rigorously, such as for instance SpaceEx, Ptolemy (based on the super-dense time semantics in), and Zélus (based on the non-standard semantics); and those who use informal approach for model definition such as Simulink, Modelica language and its associated tools. All these modelling and simulation tools share the same approach of hybrid model execution alternating between continuous evolution and sequences of discrete switchings as defined by the notion of hybrid automata. For all of these tools, the operational semantics of continuous dynamics (differential equations) is not included in the core semantic model: numerical solvers execute the continuous behaviour by advancing time and computing the values of physical continuous variables. None of the above tools have a Zeno-free semantic model. They all rely on analyzing the solver output at each integration time step, with the solver behaviour at the Zeno-limit point being usually unspecified. In this dissertation we focus on the first two steps above. In particular, we focus on proposing a rigorous Zeno-free computational framework for hybrid semantic model design, and how this Zeno-free computational framework can be implemented in the design of hybrid systems simulators. The first part of our contribution is to propose non-standard semantics for Zeno executions of hybrid systems models. This is based on interpreting Zeno executions in a non-standard densely ordered hybrid time domain. The advantages of using non- standard semantics in the analysis of Zeno behaviour is that it allows for solutions of Zeno hybrid models to be well-defined beyond the Zeno limit points, as well as representing the complex interaction between continuous and discrete dynamics in a concrete way: 1. The continuous dynamics of the hybrid system is reduced to the recurrence equation that represents the infinite iteration of infinitesimal discrete changes with infinitesimal duration. Therefore, we can handle the hybrid dynamics based only on fully discrete paradigm. 2. The representation of dynamics based on non-standard analysis is complete and the exact limit point of discrete change, like chattering-Zeno and geometric-Zeno limit points, can be handled. The second part of our contribution is to propose a rigorous Zeno-free computational framework for hybrid semantic model design and implementation. The key idea in our proposed computational framework is to perform Zeno detection and avoidance by using behavioral analysis of the system, instead of only considering zero-crossings in a hybrid time domain. The behavioral analysis technique we propose for treating Zeno is based on analyzing both types of Zeno systematically. We provide formal conditions on when the simulated models of hybrid systems display chattering-Zeno and geometric-Zeno executions. We also provide methods for carrying solutions beyond Zeno. The issue of existence and uniqueness of solution beyond Zeno is also studied in this dissertation. Our Zeno-free computational framework allows sacrificing the notion of Zeno-freeness as: i) the decision on whether or not the Zeno limiting state is chattering-Zeno or geometric-Zeno is based on formal conditions explicitly defined and provided to the hybrid simulator’s solver, and ii) the correct notion of solution beyond Zeno is well defined and established in our framework. Our approach also supports mixing compile-time transformations of hybrid programs (i.e. generating what is necessary for Zeno detection and avoidance), the decision, in run-time, for the urgent transition from pre-Zeno to post-Zeno state (based on formal conditions for the existence of Zeno), and the computation, in run-time, of the system dynamics beyond Zeno. Examples of hybrid systems with domains, guard sets, vector fields, and reset maps, illustrating the use of the methods proposed in this dissertation, are also provided.
Complete list of metadatas

https://hal.inria.fr/tel-01614081
Contributor : Ayman Aljarbouh <>
Submitted on : Tuesday, October 10, 2017 - 2:23:20 PM
Last modification on : Friday, September 13, 2019 - 9:48:42 AM

File

Thèse.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01614081, version 1

Citation

Ayman Aljarbouh. Accelerated Simulation of Hybrid Systems : Method combining static analysis and run-time execution analysis.. Computer Science [cs]. Université de Rennes 1, France, 2017. English. ⟨tel-01614081⟩

Share

Metrics

Record views

454

Files downloads

431