BisoUS — Meilleure synthèse pour les systèmes quantitatifs sous-spécifiés

Les systèmes informatisés sont omniprésents et l'identification de leurs défauts est cruciale dès les premières phases de développement, quand de nombreux aspects, comme les environnements d'exécution, n'ont pas encore été fixés. La vérification doit alors se faire sur des systèmes sous-spécifiés et, de façon contradictoire, apporter des réponses aussi informatives que possible. Dans ce projet, nous développons des techniques de vérification pour ces systèmes, en prenant en compte ce besoin d'explicabilité, par l'optimisation de ressources telles que l'énergie ou la mémoire, et la synthèse de contraintes sur les aspects sous-spécifiés, garantissant le bon fonctionnement du système. Au delà des formalismes classiques, nous considérons leurs extensions simultanées dans trois directions: des coûts pour les ressources, des paramètres pour les caractéristiques inconnues, et des jeux pour représenter tous les comportements du systèmes sous-spécifié. Le problème principal des formalismes très expressifs que nous voulons étudier et promouvoir, est que les problèmes de vérification et de synthèse associés sont très complexes, au sens algorithmique du terme, ce qui se traduit par une utilisation du processeur et de la mémoire rédhibitoires en pratique. Les problèmes de décision liés sont aussi le plus souvent indécidables. Pour attaquer ce problème, nous suivons deux approches complémentaires. D'une part, et c'est la voie la plus souvent explorée pour ce type de situations, nous identifions deux sous-classes du formalisme général qui modélisent bien certaines applications ciblées et pour lesquelles nous pensons pouvoir obtenir de meilleurs résultats théoriques et pratiques D'autre part, nous proposons le développement d'algorithmes spécifiques fonctionnant sur le formalisme général mais aux résultats fournissant des résultats approchés accompagnés de garanties formelles sur l'approximation réalisée.