|
12-12 janv. 2022 Gif-sur-Yvette (France)
|
|
|
|
|
Mercredi 12 janvier 2022 - 13h45 en visio Nous avons le plaisir de vous inviter à la première réunion du GT HiFi : Méthodes Formelles et Programmation Haute Fidélité pour Systèmes Critiques Émergents. Pour plus d'informations sur le GT Hifi, vous pouvez consulter la page suivante. Lieu La journée se déroulera intégralement en visio-conférence. Le lien Zoom est le suivant: https://inp-toulouse-fr.zoom.us/j/93107252127?pwd=bThPbm9BZHU2cEZZdDlwYW5GcWpPUT09 La conférence débutera à 13h45.
Programme 13h45 : Ouverture (Aurélie Hurault et Sylvain Conchon) 14h00 : Laurent Fribourg (LMF) Application de la méthode d'Euler à la génération d'ensembles d'états attractifs pour des systèmes dynamiques La méthode (explicite) d'Euler est une méthode du 18e siècle permettant le calcul approché de solutions d'équations différentielles. Il y a quelques années, nous avons donné une formule majorant la différence (“erreur”) entre cette solution approchée et la solution exacte. Grâce à cette marge d'erreur, on peut construire des “ensembles attractifs” du système, c'est-à-dire des ensemble d'états vers lequel le système est attiré et d'où il ne sort jamais. On montrera une application de cette construction au contrôle du bras d'un exosquelette utilisé par le laboratoire LURPA de l'ENS Paris-Saclay.
14h30 : Thierry Lecomte (Clearsy)
Méthodes formelles pour systèmes critiques: REX et perspectives
Les systèmes critiques se doivent de respecter un cadre normatif dépendant du domaine applicatif dans lequel ils évoluent et qui laisse une place variable aux méthodes formelles. Cette présentation fait le point sur 20 années d'utilisation de B, Event-B, preuve de théorèmes et model-checking pour la vérification de spécification système, la validation de paramètres, ainsi que pour le développement de programmes sans défaut et leur exécution sur plateforme sûre. Ces résultats sont mis en perspective des besoins actuels en mobilité autonome et des contraintes techniques et réglementaires associées.
Conception correcte par construction de systèmes hybrides
Les systèmes hybrides incorporent au même niveau des éléments discrets et continus, deux mondes radicalement différents. Cette intégration forte entre ces deux aspects les rend particulièrement difficiles à concevoir et certifier. Le but de notre travail est de proposer une méthodologie outillée pour la conception formelle de systèmes hybrides, en se basant sur la méthode Event-B. Cette dernière nous apporte un langage expressif et précis, permettant d'exprimer les concepts complexes nécessaires à la description de comportements continus, tout en étant fondamentalement basée sur des états et des transitions, adaptés aux aspects discrets. De surcroît, Event-B propose une opération de raffinement, centrale dans l'approche correcte-par-construction, et que l'on peut enrichir afin de proposer des opérations propres aux systèmes hybrides, tels que l’approximation.
15h30 : pause
15h45 : Alexandra Halchin (RATP)
Utilisation industrielle par la RATP d'une démarche de Preuve d'Evaluation par Rétro-modélisation Formelle (PERF) dans le cadre de ses projets de modernisation du métro impliquant le déploiement de systèmes critiques temps-réel distribués/embarqués » (contexte / enjeux / démarche & méthode / Retour d'expérience / perspectives)
Une sémantique constructive exécutable pour un langage déclaratif synchrone avec automates hiérarchiques
Un langage tel que Scade permet d'écrire un modèle synchrone dans lequel des équations à flot-de-données et des automates hiérarchiques peuvent être composés arbitrairement. Deux sémantiques ont été proposées par le passé: (i) une sémantique indirecte dîte par traduction, c'est-à-dire que les automates hiérarchiques et autres structures de contrôle sont réécrites vers le sous-ensemble flot-de-données du langage qui est ensuite compilé vers du code impératif; (ii) une sémantique relationnelle directe qui exprime ce qu'est une bonne réaction synchrone à chaque instant mais abstrait volontairement la manière de la construire, son existence et son unicité éventuelles. Elle est simple mais non exécutable. Dans cet exposé, nous présentons une sémantique exécutable qui s'applique directement au source avant toute étape du compilateur, y compris le typage. Elle conduit à la définition d'un interprète de référence indépendant du compilateur. Celui-ci peut être utilisé pour tester le compilateur ou mettre au point des modèles imcomplets ou rejetés par le compilateur. Cette sémantique s'appuie sur une interprétation co-itérative des flots, chaque élément étant obtenu par une itération de point-fixe finie. Nous montrerons quelques exemples et la structure de l'interprète écrit dans un style purement fonctionnel, en OCaml. Nous illustrerons sur des exemples les différences vis-à-vis de la sémantique constructive d'Esterel et, en particulier, ce qu'elle dit des circuits cycliques. Ce travail est mené avec Jean-Louis Colaço.
16h45 : Pierre-Loïc Garoche (ENAC)
Partitionnement de domaines abstraits
Dans cette présentation, nous ferons un bref aperçu des méthodes de partitionnements de domaines abstraits (numériques) et proposerons une alternative moins couteuse et néanmoins expressive au partitionnement par BDD comme proposé par Chen et Cousot en 2005 ou implementé par Bertrand Jeannet dans BDDAPRON quelques années plus tard.
17h15 : Clôture (Aurélie Hurault et Sylvain Conchon) |
| Personnes connectées : 1 | Vie privée |
|
