ACTION COOPERATIVE INRIA

PRESYSA

Cette action se situe dans l'axe intitulé développement de logiciels certifiés. Elle concerne la vérification de systèmes synchrones et asynchrones ayant un nombre d'états infinis en se concentrant sur les propriétés de sûreté et d' invariance.

Actuellement, les méthodes algorithmiques ne peuvent être utilisées que sur des systèmes infinis particuliers. Par ailleurs, les méthodes déductives sont difficiles à mettre-en-oeuvre et demandent un fort investissement. Pour cette raison, l'automatisation et l'intégration des méthodes de vérification sont des facteurs clés dans le succès d'un assistant de preuve.

Les techniques d'automatisation de la preuve que nous proposons d'utiliser sont basées sur la réécriture. L'intégration des méthodes de vérification se fera en particulier par combinaison de preuve déductive et de model-checking, en se basant sur des techniques d'interprétation abstraite.

Dans ce cadre, nous nous proposons d'étudier les questions liées à la modélisation de systèmes et à la réalisation de preuves sur des cas significatifs. Nous avons déterminé deux domaines privilégiés pour lesquelles une modélisation par réécriture est relativement simple: programmes synchrones et protocoles communicants par échanges de messages.

PARTICIPANTS

CMI, Marseille

VERIMAG, Grenoble

LORIA, Nancy

IRISA, Rennes

LIFC, Besancon