CE48 - Fondements du numérique : informatique, automatique, traitement du signal

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

Résumé de soumission

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.

Coordination du projet

didier lime (Ecole Centrale de Nantes)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

IRISA Institut de Recherche en Informatique et Systèmes Aléatoires
LIPN Université Sorbonne Paris Nord (Paris 13)
LS2N Ecole Centrale de Nantes
LMF UPSaclay - Laboratoire Méthodes Formelles

Aide de l'ANR 409 023 euros
Début et durée du projet scientifique : mars 2023 - 48 Mois

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter