Vous êtes ici

Property-Driven Abstraction of Dynamical and Hybrid Systems

Equipe et encadrants
Département / Equipe: 
Site Web Equipe: 
https://team.inria.fr/hycomes/
Directeur de thèse
Benoît Caillaud
Co-directeur(s), co-encadrant(s)
Khalil Ghorbal
Contact(s)
NomAdresse e-mail
Khalil Ghorbal
khalil.ghorbal@inria.fr
Sujet de thèse
Descriptif

The general context of the thesis is that of the design of (multiphysical) avionic air systems, based on their modeling at various scales and abstraction levels (such as precise thermodynamics or controllable dynamic models), some of which are in the Modelica specification language. These are critical systems whose validation, by test, simulation and/or by formal methods is crucial.

A recurring difficulty of the simulation of models involving differential equa- tions with control laws is the handling of mode changes (zero-crossing in Matlab / simulink, multimode DAEs in Modelica etc.). These problems are non-trivial, and both the literature and industrial experiments show the limitations of the solvers that are currently used in Simulink or Modelica / Dymola tools. Several recent works address this problem, where the authors develop methods for the correct simulation of multi-physical systems described by multi-mode DAEs. In such cases, the numerical simulation, so-called robust or guaranteed simulation, computes at once sets of traces (reachable sets) instead of single simulations. These guaranteed methods also make it possible to validate behavioral and temporal properties, thus also allowing the comparison of models.

In general, the abstraction of hybrid systems, whether based on algebraic techniques, topology, or sets, is the basis of formal verification tools. Several methods were derived from program analysis or proof systems. All these aspects are at the heart of the INRIA Project Lab "IPL ModeliScale" which will provide an ideal scientific context for the PhD student. The application of such methods to the industrial case study proposed by Liebherr will be studied in the longer term. 

Bibliographie
  1. [1]  Albert Benveniste, Timothy Bourke, Benoît Caillaud, and Marc Pouzet. Non-standard semantics of hybrid systems modelers. J. Comput. Syst. Sci., 78(3):877–910, 2012.

  2. [2]  Albert Benveniste, Benoit Caillaud, Hilding Elmqvist, Khalil Ghorba- land Martin Otter, and Marc Pouzet. Structural analysis of multi-mode dae systems. In HSCC, 2017.

  3. [3]  Olivier Bouissou, Eric Goubault, Sylvie Putot, Karim Tekkal, and Franck Védrine. Hybridfluctuat: A static analyzer of numerical programs within a continuous environment. In Computer Aided Verification, 21st Interna- tional Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, 2009.

  4. [4]  Timothy Bourke and Marc Pouzet. Zélus: a synchronous language with odes. In HSCC, pages 113–118. ACM, 2013.

    [5]  David Delmas, Eric Goubault, Sylvie Putot, Jean Souyris, Karim Tekkal, and Franck Védrine. Towards an industrial use of FLUCTUAT on safety- critical avionics software. In Formal Methods for Industrial Critical Sys- tems, 14th International Workshop, FMICS 2009, Eindhoven, The Nether- lands, November 2-3, 2009. Proceedings, 2009.

    [6]  Laurent Fribourg, Eric Goubault, Sylvie Putot, and Sameh Mohamed. A topological method for finding invariant sets of switched systems. In HSCC, pages 61–70. ACM, 2016.

    [7]  Khalil Ghorbal and André Platzer. Characterizing algebraic invariants by differential radical invariants. In TACAS, volume 8413 of Lecture Notes in Computer Science, pages 279–294. Springer, 2014.

    [8]  Eric Goubault. Static analysis by abstract interpretation of numerical pro- grams and systems, and FLUCTUAT. In Static Analysis - 20th Interna- tional Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Pro- ceedings, 2013.

    [9]  Eric Goubault, Jacques-Henri Jourdan, Sylvie Putot, and Sriram Sankara- narayanan. Finding non-polynomial positive invariants and lyapunov func- tions for polynomial systems through darboux polynomials. In American Control Conference, ACC 2014, Portland, OR, USA, June 4-6, 2014, 2014.

    [10]  Eric Goubault, Olivier Mullier, Sylvie Putot, and Michel Kieffer. Inner approximated reachability analysis. In HSCC, pages 163–172. ACM, 2014.

    [11]  Eric Goubault and Sylvie Putot. A zonotopic framework for functional abstractions. Formal Methods in System Design, 47(3), 2015.

    [12]  Eric Goubault and Sylvie Putot. Forward inner-approximated reachability of non-linear continuous systems. In HSCC, 2017.

    [13]  Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer. Formal verification of ACAS x, an industrial airborne collision avoidance system. In 2015 Inter- national Conference on Embedded Software, EMSOFT 2015, Amsterdam, Netherlands, October 4-9, 2015, 2015.

    [14]  Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, and André Platzer. A method for invariant generation for polynomial continuous systems. In VMCAI, volume 9583 of Lecture Notes in Computer Science, pages 268– 288. Springer, 2016.

    [15]  Andrew Sogokon, Khalil Ghorbal, and Taylor T. Johnson. Decoupling abstractions of non-linear ordinary differential equations. In FM, volume 9995 of Lecture Notes in Computer Science, pages 628–644, 2016. 

Début des travaux: 
Fall 2018
Mots clés: 
Cyber-physical systems, hybrid systems, DAE, Modelica, Guaranteed simulation, Static aanlysis, Proofs
Lieu: 
IRISA - Campus universitaire de Beaulieu, Rennes