Synthèse Multicritère de Systèmes Réactifs : Fondations, Algorithmes et Outils

Nous vivons l’ère de l’intelligence ambiante : nous sommes entourés de systèmes (informatiques) réactifs (SIRs) qui interagissent continuellement avec leur environnement via des instructions utilisateur, des senseurs, etc. Leur exactitude est souvent cruciale, soit pour des raisons de sécurité (p.ex. ABS), soit pour des contraintes de production de masse (p.ex. smartphones). Néanmoins, leur conception est complexe et sujette aux erreurs. La vérification formelle et la synthèse sont deux réussites de l’informatique, qui ont pour but la construction automatique de contrôleurs fiables pour les SIRs. Beaucoup de techniques se fondent sur la théorie des jeux, modélisant les interactions entre le SIR et son environnement sous forme de jeu compétitif.

Au cours de la dernière décennie, le domaine a évolué des spécifications Booléennes vers celles dites quantitatives, donnant naissance à des modèles capables de décrire la performance de SIRs. Cependant, les modèles actuels ne permettent de représenter qu’un seul aspect quantitatif (ou qualitatif) à la fois : ils ne tiennent pas compte de leurs interactions et des compromis en résultant. De tels compromis peuvent apparaître entre différentes ressources (p.ex. diminuer le temps de réponse requiert plus de puissance de calcul et de consommation énergétique) mais aussi entre différents modèles comportementaux (p.ex. performance dans le pire des cas vs. en moyenne). Ces interactions sont au coeur des scénarios réels et demandent que les développeurs décident de l’équilibre entre différents aspects. Il est donc nécessaire de fournir des modèles et des outils capables de représenter ces interactions pour que la synthèse soit efficace en pratique.

L’objectif de ce projet est de mettre en place la prochaine génération de techniques de synthèse en établissant les bases formelles, les algorithmes et les outils nécessaires pour changer de paradigme, depuis les modèles qualitatifs et quantitatifs monocritères vers les multicritères.