CE40 - Mathématiques, informatique théorique, automatique et traitement du signal

Techniques et outils efficaces pour la vérification et synthèse des systèmes temps-réels – TickTac

Résumé de soumission

La vérification formelle, et en particulier le model checking, consiste à assurer la correction des systèmes critiques. La correction d'un grand nombre de systèmes temps-réels dépend, non seulement du bon calcul des valeurs de sortie en fonction des entrées, mais aussi des mesures quantitatives comme le temps d'exécution et la consommation d'énergie. Les formalismes de model checking pour les systèmes à états finis permettent souvent la définition d'une notion de temps, souvent par la discrétisation du domaine de temps. Cependant, cette modélisation n'est pas toujours suffisamment précise, et fait augmenter la taille de l'espace d'états de manière prohibitive, rendant la vérification trop coûteuse.

Les automates temporisés sont un formalisme standard pour modéliser des systèmes avec des contraintes de temps, pour lesquels des algorithmes et outils efficaces ont été développés. Ces outils ont eu un impact significatif dans la vérification des systèmes temps-réels. Il reste cependant des verrous qu'il faut résoudre pour pouvoir traiter de systèmes de plus grande taille. Si les techniques actuelles sont particulièrement efficaces pour le traitement des contraintes de temps, la taille de l'espace d'états discrets est toujours un problème. Plusieurs idées qui proviennent du model checking pour états finis, tels que le raffinement d'abstraction, les abstractions dynamiques, la réduction par ordre partiel n'ont pas été complètement exploité dans le cadre temporisé. Les algorithmes pour les spécifications de vivacité ou les problèmes d'optimisation n'ont pas reçu suffisamment d'attention non plus du point de vue de l'efficacité, ce qui rend les outils de vérification moins intéressants pour l'utilisateur. Enfin, les outils existants sont principalement basés sur le même type d'algorithmes et n'exploitent pas suffisamment la possibilité de développer des techniques sur mesure pour certains types d'application, afin d'obtenir une panoplie d'outils complémentaires.

Le but de ce projet est de surmonter certains obstacles pour passer à l'échelle dans la vérification et la synthèse des automates temporisés en étudiant de nouveaux algorithmes et structures de données alternatifs, des spécifications riches, des techniques d'abstraction. Un outil libre sera développé et maintenu pour valider ces résultats, et appliqué à la planification de mouvement pour la robotique, l'analyse de performance dans les systèmes ferroviaires, et dans d'autres collaborations que nous avons avec nos partenaires. Le développement de l'outil libre sera au coeur de ce projet; il contiendra les algorithmes connus et ceux qui seront développés dans ce projet pour les diverses extensions des automates temporisés pour la vérification, la synthèse, et les problèmes d'optimisation. Le format d'entrée sera compatible avec les model checkers existants pour permettre une comparaison systématique entre les algorithmes et les outils. Les membres du consortium ont contribué aux plus récents développements sur les méthodes de vérification les plus efficaces, et ont de l'expérience en développement d'outil. Notre objectif est de rendre les automates temporisés plus attractif en enrichissant les spécifications et les systèmes qu'on peut analyser, et en rendant les algorithmes plus efficaces ; en rendant ainsi les automates temporisés l'outil de choix pour les systèmes temps-réels.

Coordination du projet

Ocan Sankur (Institut de Recherche en Informatique et Systèmes Aléatoires)

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

LIS Laboratoire d'Informatique et Systèmes
IRISA Institut de Recherche en Informatique et Systèmes Aléatoires
EPITA ECOLE POUR L'INFORMATIQUE ET LES TECHNIQUES AVANCEES
LSV Laboratoire Spécification et Vérification
ISIR Institut des Systèmes Intelligents et Robotiques
LaBRI Laboratoire Bordelais de Recherche en Informatique

Aide de l'ANR 303 947 euros
Début et durée du projet scientifique : février 2019 - 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