ARC: projet de recherche "Non-Zero Sum Game Graphs"

Les systèmes réactifs sont des systèmes informatiques qui maintiennent une interaction constante avec l’environnement dans lequel ils opèrent. Les systèmes informatiques qui automatisent les transports publics, les systèmes d’aide au pilotage d’avion, ou encore les systèmes informatiques qui contrôlent les appareillages médicaux sont des exemples de systèmes réactifs. Toute défaillance ou tout bug dans ces contextes critiques peuvent avoir des conséquences catastrophiques.

Les systèmes réactifs ont plusieurs caractéristiques (opérations en temps-réel, parallélisme, simultanéité des évènements, etc.) qui les rendent difficiles à concevoir. Pour rencontrer ces difficultés, des recherches fondamentales visent à développer de nouveaux modèles mathématiques qui permettent d’exprimer précisément les propriétés de correction que doivent satisfaire ces systèmes. Ces méthodes mathématiques permettent ensuite de prouver mathématiquement la correction d’une solution ou de trouver systématiquement des erreurs de conception avant la mise en place du système. Le "model-checking" est une technique qui a révolutionné le développement des systèmes critiques en permettant la détection d’erreur de conception très tôt dans le cycle de développement et ceci de manière automatique.

Une autre méthode plus ambitieuse, appelée "synthèse", est au cœur de ce projet de recherche: elle consiste à proposer des techniques (modèles, algorithmes, outils informatiques) qui permettent de synthétiser un système correct, au regard des spécifications demandées et de son environnement, à l’aide d’un algorithme. Cette technique vise donc à permettre la construction automatisée de systèmes corrects à partir de leurs spécifications.

Cette nouvelle méthode innovante est au cœur de ce projet ARC, mené par l’équipe des "Méthodes formelles et vérification" (Département d'Informatique, Faculté des Sciences).

Porte-parole

Jean-François Raskin
Méthodes formelles et vérification
Faculté des Sciences