Modélisation fonctionnelle et preuve de circuits avec LP / Michel Allemand ; sous la direction de J.-L. Paillet

Bibliogr. p.155-164

Thèse de doctorat informatique 1995 Aix-Marseille 1

Les méthodes formelles présentent des potentialités intéressantes dans le cadre de la vérification de la correction des systèmes digitaux. Cette thèse propose un système formel, le P-calcul, permettant une modélisation fonctionnelle des circuits orientée vérification formelle. Des méthodologies de preuves adaptées au démonstrateur utilisé, le Larch-Prover (LP) ainsi qu'a cette modélisation sont décrites. Dans une première partie, nous définissons un langage typé permettant de décrire les structures des circuits. Nous en donnons ensuite une interprétation dans un modèle fonctionnel, qui représente les comportements associés. Les règles de transformations que nous avons proposées sous la forme d'un système de réécriture permettent l'obtention d'une forme normale pour les expressions du langage. On peut alors, entre autre, définir un procédé de reconnaissance des circuits synchrones et donner un algorithme de construction des solutions des équations récursives décrivant les circuits avec boucles. Puis, les expressions du P-calcul sont traduites dans la syntaxe du Larch-Prover. Après avoir construit une base de propriétés arithmétiques prouvées, nous proposons deux méthodes pour vérifier que l’implémentation d'un circuit est correcte, selon que sa spécification est une définition inductive ou une liste de propriétés, et dans ce dernier cas elle n'est pas forcément complète. Ces méthodes sont appliquées à plusieurs circuits qui ont été proposés, ces dernières années, dans la communauté internationale