Skip to Main content Skip to Navigation
Theses

Analyse statique par interprétation abstraite de systèmes hybrides.

Olivier Bouissou 1
1 LMeASI - Laboratoire Modélisation et Analyse de Systèmes en Interaction
LIST - Laboratoire d'Intégration des Systèmes et des Technologies : DRT/LIST
Abstract : The power and efficiency of abstract interpretation based static analysis methods for the verification of safety critical embedded software is no longer to be outlined. However, the precision of the analysers needs now to be reinforced. The use of ever more sophisticated relational abstract domains make it possible to reduce the overapproximation that limits the power of simpler domains, but the precision of the latest analysers is still constrained by the precision of the input values. These are given by a sensor that measures some physical phenomena, and they are generally overapproximated by an interval. In order to deal better with these continuous inputs, one may analyse, in addition to the program itself, the physical environment in which the program is executed. In this way, we obtain a more complex system which has both a discrete dynamics (the program) and a continuous one (the environment). Such hybrid systems are generally studied using extensions of finite automata or process calculi that introduce a continuous dynamics. The use of model-checking techniques still suffers from a combinatorial explosion that prohibits the use of such models for the analysis of large safety critical embedded programs. The first contribution of this thesis is to provide an extension of imperative programming lan- guages that describes both the program, the external environment and the interactions between both. The physical environment is described as a set of differential equations, each of them re- presenting a continuous mode. The interactions between the program and the environment are modeled using two extra keywords that represent the effect of sensors and actuators. A denota- tional semantics is given to the whole system (the program and the environment together). This semantics remains very close to the standard denotational semantics of imperative languages. The main difficulty was to define a semantics for the continuous part of the system : we express the solutions of differential equations as the fixpoint of a monotone operator in a CPO, and we show that Kleene's iteration converges towards this fixpoint. The second contribution is an abstract interpretation based static analysis of these hybrid systems. Our method has two stages. First, under some assumptions on the program to be ana- lysed, a partitioning of the space of the input variables is built. For that, we combine a forward reachability method with an interval based analysis. In this way, we obtain an abstraction of the impact of the program on the continuous evolution : the continuous space is divided into zones in which we know that an actuator will be activated. The second stage of the analysis use this partitioning and a guaranteed integration of differential equations algorithm in order to build a safe overaproximation of the continuous evolution. A prototype analyser using these techniques was implemented and the first results on examples of hybrid systems from the literature show good results. Finally, the third contribution of this thesis is a new guaranteed integration algorithm named GRKLib. Unlike existing methods, GRKLib is based on a non-validated, numerical integration scheme (we chose an order 5 Runge-Kutta method, but any other algorithm works). The global error made during the numerical integration is then computed using interval arithmetic. This error is expressed as the sum of three terms : the one-step error, the propagation error and the computation error due to the use of floating point numbers. Each term is computed separately and advanced techniques are used in order to reduce them and control the integration step size so that the growth of the global error is limited. A C++ library implementing these concepts was developed and the results presented in this thesis are very promising.
Document type :
Theses
Complete list of metadatas

Cited literature [104 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/pastel-00004412
Contributor : Ecole Polytechnique <>
Submitted on : Wednesday, July 21, 2010 - 3:04:40 PM
Last modification on : Monday, February 10, 2020 - 6:12:32 PM
Long-term archiving on: : Tuesday, October 23, 2012 - 10:35:32 AM

Identifiers

  • HAL Id : pastel-00004412, version 1

Collections

Citation

Olivier Bouissou. Analyse statique par interprétation abstraite de systèmes hybrides.. Informatique [cs]. Ecole Polytechnique X, 2008. Français. ⟨pastel-00004412⟩

Share

Metrics

Record views

559

Files downloads

798