February 8, 2021

Guillaume Dupont (INP Toulouse)

Les systèmes hybrides sont des systèmes qui intègrent des comportements discrets (ordinateurs, calculateurs) et des comportements continus (phénomènes physiques à contrôler). Les systèmes hybrides sont variés et versatiles, et de ce fait occupent une place de plus en plus importante dans notre vie quotidienne, que ce soit dans le cadre d’objets connectés ou pour des applications critiques telles que des voitures autonomes ou des avions.

La nature hybride de ces systèmes les rend particulièrement difficiles à vérifier : les méthodes formelles classiques sont adaptées à leurs parties discrètes, et leurs parties continues est l’objet d’étude de la théorie du contrôle, mais intégrer ces deux aspects au même niveau dans le processus de conception et de vérification de ces systèmes est encore un défi majeur du domaine.

Dans le cadre de nos travaux, nous avons mis au point un cadre formel dont le but est la conception correcte par construction de systèmes hybrides. Ce cadre se base sur la méthode Event-B, dont il exploite le mécanisme d’extension ainsi que l’opération de raffinement, afin de mettre à disposition un ensemble de patrons de conception formels, qui peuvent être utilisés et réutilisés pour concevoir tout type de système hybride, de manière incrémentale. Ces patrons ont été formellement prouvés en utilisant les outils de preuve de Event-B. Ce cadre sert par ailleurs de support à une méthode générique de conception formelle de ces systèmes, que nous illustrons sur divers études de cas.