SMV et Coq

Pablo Argon

Cadence Berkeley Labs

L'outil de vérification Cadence-SMV, conçu et développé par Kenneth McMillan, permet de vérifier des propriétés temporelles de systèmes de grande taille, voire infinis, grâce à la combinaison d'une vérificateur sur modèle symbolique et d'un prouveur spécialisé. Son intérêt pratique a déjà été mis en évidence sur de nombreux exemples industriels : preuve de l'algorithme de Tomasulo, preuve de plusieurs "cache coherence protocols", etc. Cependant, dans l'implémentation actuelle du système plusieurs erreurs ont été relevées, particulièrement dans le prouveur spécialisé

Pour cette raison, depuis environ un an, nous avons formalisé une version simplifiée du prouveur spécialisé de SMV (toutes les règles n'ont pas été traitées) dans l'assistant à la preuve Coq, afin de pouvoir à la fois prouver la correction des règles de décomposition, et extraire le code implémentant la décomposition, c'est-à-dire le prouveur spécialisé, grâce aux techniques de certification et d'extraction de programmes uniques de Coq.

Dans cet exposé nous donnerons un aperçu de ce travail en présentant les principales étapes suivies pour arriver au <> du nouveau système SMV basé sur un prouveur spécialisé extrait depuis la preuve formelle faite en Coq et interfacé avec un vérificateur sur modèle développé spécialement.

Back to schedule.