JOURNÉE HIFI : MERCREDI 12 JANVIER 2022
A la première réunion du GT HiFi : Méthodes Formelles et Programmation Haute Fidélité pour Systèmes Critiques Émergentsn Guillaume Dupont a présenté
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.