Analyse automatique de détection d'erreur des systèmes à compteurs

Les systèmes concurrents sont de plus en plus répandus à mesure que des progrès sont réalisés sur les architectures de multiprocesseurs, les appareils peu gourmands en énergie, ainsi que l’informatique moléculaire. Il est impératif d’éviter les failles de sécurité subtiles dans les systèmes concurrents, mais les approches traditionnelles du génie logiciel telles que le test ne gèrent pas la concurrence. La vérification formelle, une approche ancrée dans l’informatique théorique, permet de prévenir les erreurs de manière rigoureuse. Elle a été utilisée avec succès au cours des dernières décennies afin de vérifier les systèmes critiques. Des efforts sont déployés afin d’amener la vérification formelle vers le développement logiciel avec des cycles de développements plus courts. Pour atteindre cet objectif, les procédures de vérification doivent (a) être aussi automatisées que possible; (b) s’éloigner du paradigme des systèmes à états finis; et (c) se concentrer sur la recherche d’erreurs plutôt que sur la démonstration de leur absence.

Je propose donc un cadre de détection automatique d’erreur pour les systèmes à compteurs. Inspiré par le récent succès des logiques d’erreur pour l’analyse de programmes, les progrès des technologies SAT/SMT et les performances de l’intelligence artificielle, l’objectif de cette demande est de fournir des solveurs de pointe à usage général permettant une détection rapide à grande échelle d’erreur dans les systèmes concurrents. Cet objectif sera atteint (i) en développant un cadre de «model checking orienté» pour les réseaux de Pétri, afin de briser le plafond des algorithmes exacts avec des complexités calculatoires prohibitives; (ii) en démontrant l’applicabilité et l’efficacité de cette théorie à la vérification de programmes; et (iii) en généralisant ces travaux à des systèmes à compteurs plus expressifs.