Laboratoire d'Informatique de Grenoble

Conception correcte par construction de systèmes hybrides

Résumé

Les systèmes hybrides sont des systèmes qui incorporent simultanément des comportements discrets (contrôleurs) et continus (phénomènes physiques).
 De par cette nature hybride, ces systèmes sont difficiles à modéliser et à vérifier : si les aspects discrets peuvent être pris en charge par les méthodes formelles usuellement utilisées en informatique, les aspects continus sont eux mieux décrits avec la théorie du contrôle.
Dans le cadre de nos travaux de recherche, nous avons proposé une extension formelle à la méthode Event-B, qui permet de manipuler les aspects discrets et continus de systèmes hybrides au même niveau dans la modélisation et dans la preuve. Cette extension prend la forme d'un cadre (ou "framework"), qui se compose de divers composants et patrons de conception, destinés à la conception formelle et haut-niveau de tels systèmes.