MEA

  • Posted on: 13 November 2017
  • By: admin
  • Updated on: 4 December 2017
Date: 
14-12-17
Détails: 

Chers collègues,

Comme annoncé précédemment et pour finaliser la préparation du nouveau GT VS-CPS Verification et Synthèse de Systèmes Cyber-Physiques proposé dans le cadre du renouvellement du GDR MACS 2019-2023, nous organisons une réunion dans le cadre du GT MEA.

La réunion aura lieu le

Jeudi 14 Décembre 2017, 10h-17h

au

CNAM
292 rue Saint-Martin, Paris,  métro Réaumur Sébastopol.
salle 11A3 (Accès 11A, 3ème étage).

Cette première réunion  de travail du GT VS-CPS nous permettra d'affiner ensemble les objectifs du GT ainsi que nos attentes vis à vis du nouveau groupe.  
Elle prendra la forme d’une série d’exposés de 20mn max afin de permettre au plus grand nombre de prendre la parole, suivie d’une période d’interaction et discussion.

Le programme est maintenant finalisé .

Pour mémoire, je rappelle la problématique scientifique motivant la création du GT VS_CPS :  

Les systèmes cyber-physiques (CPS) résultent de l’intégration de composants informatiques à des systèmes physiques. Ces composants informatiques, disposant de capacités de communication et de calcul, collaborent pour surveiller et contrôler les processus physiques via des boucles de rétroactions. Les applications des CPS sont nombreuses (robotique, véhicule autonome, bâtiment intelligent, etc.) et promettent d’impacter la société dans tous les domaines (habitat, transport, santé et autonomie, industrie, énergie, etc.). Les CPS évoluent souvent dans un environnement dynamique et incertain, et en même temps, sont soumis à des exigences critiques de sûreté/sécurité qui nécessitent d’être prises en compte dès les premiers stades de conception. Ainsi, il est crucial de développer des outils méthodologiques, basés sur des modèles, pour la vérification et la synthèse « correcte par construction » d’algorithmes de surveillance, de contrôle et de reconfiguration des CPS permettant un fonctionnement sûr en dépit d’incertitudes environnementales importantes. Sur le plan méthodologique, le nouveau GT VS-CPS traitera de la modélisation et de la spécification des CPS, de leur vérification et de leur synthèse par des méthodes dites « formelles » : méthodes ensemblistes au sens large (incluant aussi les problèmes de satisfiabilité (SAT) et les problèmes de satisfaction de contraintes), abstraction discrète et contrôle symbolique, optimisation robuste, etc.

========================================================================

Programme de la journée :

1.    Le GT VS CPS. Motivations et contexte scientifique.  Nacim Ramdani, Antoine Girard et Luc Jaulin.

2.    Exposés scientifiques (20mn + questions, par exposé).  9 exposés, résumés ci-après.
    a. 10h-12h30 :            Exposés #1 à #4
    b. approx. 12h30-14h :     Pause déjeuner
    c. 14h :                 Exposés #5 à #9.

3.    Discussion, synthèse et finalisation du contour scientifique du GT VS-CPS.

###########################################################################

Exposé #1
Titre.        Zélus, un langage synchrone avec des ODEs
Auteur.      Marc Pouzet, ENS Paris.
Résumé.     Le langage synchrone Lustre a été introduit pour programmer et vérifier les systèmes de contrôle/commande réactif. Il a donné naissance au langage SCADE utilisé aujourd'hui pour réaliser les logiciels le plus critiques des avions, par exemple. Lustre se limite aux systèmes a temps discret et ne modélise ni fidèlement, ni efficacement un système hybride combinant temps discret et temps continu. Dans cet exposé, nous présenterons Zélus, une extension conservatrice de Lustre avec des ODEs qui permet d'écrire à la fois un modèle du logiciel et de l'environnement. La présentation sera illustrée d'exemples concrets de blocs (discrets/continus) de la libraire standard de Simulink. Nous verrons que certains blocs s'écrivent aisément alors que d'autres, tels que le "memory block" ou le "time delay" sont rejetés par le compilateur parce que mal typés.

Exposé #2
Author.    Pierre-Loïc Garoche (ONERA)
Title:          Vérification de contrôleurs: méthodes et problématiques à l'Onera.
Résumé: Dans cet exposé nous présenterons nos différents travaux autour de la vérification de contrôleurs. Ces travaux sont d'une part, motivés par des exemples industriels qui combinent de façon disgracieuse éléments discrets et continus, et d'autres part un effort de développer des prototypes pour permettre d'analyser ces systèmes et d'introduire les méthodes formelles au sein du développement basé modèle. Nous présenterons plus particulièrement deux thèmes: (1) nos problématiques autour de l'extraction de systèmes hybrides à partir de modèles industriels et (2) la chaîne d'outils CoCoSim pour l'analyse et la compilation de modèle Simulink/Stateflow.

Exposé #3
Titre.        Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems.
Auteur.     Victor MAGRON, VERIMAG CNRS.
Abstract. We consider the problem of approximating the reachable set of a discrete-time polynomial system from a semialgebraic set of initial conditions under general semialgebraic set constraints. Assuming inclusion in a given simple set like a box or an ellipsoid, we provide a method to compute certified outer approximations of the reachable set. The proposed method consists of building a hierarchy of relaxations for an infinite-dimensional moment problem. Under certain assumptions, the optimal value of this problem is the volume of the reachable set and the optimum solution is the restriction of the Lebesgue measure on this set. Then, one can outer approximate the reachable set as closely as desired with a hierarchy of super level sets of increasing degree polynomials. For each fixed degree, finding the coefficients of the polynomial boils down to computing the optimal solution of a convex semidefinite program. When the degree of the polynomial approximation tends to infinity, we provide strong convergence guarantees of the super level sets to the reachable set. We also present some application examples together with numerical results.

Exposé #4
Titre.        Computing an inner and an outer approximation of the forward reach space of a nonlinear continuous-time system".
Auteur.     Thomas Le Mézo, Luc Jaulin, Benoit Zerr (ENSTA Bretagne)
Abstract.  Given a nonlinear continuous-time system described by state equations of the form dx/dt=f(x(t)), the forward reach set Forw(X0) is the set of all states x(t) that can be reached for at least one t>0 and one initial state x0 in X0. We propose a method able to find a guaranteed inner and an outer approximation of Forw(X0). The method we propose combines interval analysis, positive-invariant set theory and constraints-based methods.

Exposé #5
Titre.        On the validation of nonlinear control systems via reachability analysis.
Auteur.     Nacim Meslem (Gipsa-Lab) & Nacim Ramdani (PRISME)
Abstract.  In the last few years interval methods have been successfully applied to solve many problems related to control systems theory. For instance, problems such as robust state estimation, guaranteed parameters identification, safety behaviour verification, robust feedback stabilizing controllers have already been tackled with interval methods in the bounded-error framework. This talk focuses on the use of reachability analysis to check a priori that the performance of given nominal controllers designed using simplified or nominal modelling are still satisfied when considering a comprehensive modelling and some bounded uncertainties and disturbances. After quickly reviewing interval-analysis based approaches to reachability with nonlinear continuous and hybrid system, the verification method is introduced. It is structured in three levels: 1) the desired control specifications are defined as set-membership criteria, 2) an outer-approximation of the reachable set of the closed-loop system is computed, 3) consistency techniques are finally applied. Examples will be given.

Exposé #6
Titre.        Compositional Abstraction-Based Controller Synthesis for Vehicle Platooning Using Contract Based Design
Authors.   Adnane Saoud, Antoine Girard & Laurent Fribourg; L2S & LSV
Abstract.  This talk deals with the synthesis of symbolic controllers for interconnected sampled-data systems where sampling in each component may not be synchronized. A compositional approach based on continuous-time assume-guarantee contracts is used. The theoretical results are then applied to the vehicle platooning problem. We assign an assume-guarantee contract to each vehicle and design hierarchical controllers enforcing these contracts and consisting of a low-level event-triggered controller and a high-level sampled-data controller synthesized using symbolic abstractions techniques. Numerical simulations are then presented for vehicle platooning on straight and circular roads, which show the effectiveness of our approach.

Exposé #7
Authors.   Mohammad Al Khatib, Antoine Girard & Thao Dang; L2S & Verimag
Title.        Self-triggered control for sampled-data systems using reachability analysis.
Abstract. In this presentation, we design the sampling policy in sampled-data systems. It is known that implementing such systems using variable sampling periods, instead of a constant period, is more efficient in terms of performance and resource utilization. Thus, after rewriting the system in the framework of impulsive linear systems, a self-triggered control strategy obtained using reachability analysis is proposed in order to define the sampling period as a function of the state.

Exposé #8
Authors.   A. Chapoutot, J. Alexandre dit Sandretto, O. Mullier
Title.        A CSP Approach to Design/Verify CPS
Abstract.  Cyber-physical systems mix continuous-time dynamics and sampling-based behaviors, which constantly and continuously interact each other. These two parts have to consider as a whole during the design and the verification phases in order to produce a system fulfilling expected properties. Constraint satisfaction problem is a framework allowing the description of system and properties by a set of constraints. Recently, an extension of this framework with ordinary differential equations has offered a new framework for cyber-physical systems. One of the strength of this framework is to allow the description of systems considering bounded uncertainties in models. When constraint satisfaction problems are solved with set-membership solvers reliable results are produced. An overview of this framework is given and illustrates trough examples such as robust controller synthesis, parameter design synthesis or reliable path planning algorithms.

Exposé #9
Author.     Khalil Ghorbal, Albert Benveniste, Benoit Caillaud and Marc Pouzet.
Title:        Structural Analysis of Multi-Mode DAE Systems
Resumé: Differential Algebraic Equation (DAE) systems constitute the mathematical model supporting physical modeling languages such as Modelica or Simscape. Unlike ODEs, they exhibit subtle issues because of their implicit latent equations and related differentiation index. Multi-mode DAE (mDAE) systems are much harder to deal with, not only because of their mode-dependent dynamics, but essentially because of the events and resets occurring at mode transitions. Unfortunately, the large literature devoted to the numerical analysis of DAEs do not cover the multi-mode case. It typically says nothing about mode changes. This lack of foundations causes numerous difficulties to the existing modeling tools. Some models are well handled, others are not, with no clear boundary between the two classes. In this paper, we develop a comprehensive mathematical approach to the structural analysis of mDAE systems which properly extends the usual analysis of DAE systems. We define a constructive semantics based on nonstandard analysis and show how to produce execution schemes in a systematic way.

###########################################################################