Preuves par récurrence avec ensembles couvrants contextuels. Application à la vérification de logiciels de télécommunications

• Main Author: Stratulat, Sorin
• Language: FRE
• Published: Université Henri Poincaré - Nancy I 2000
• Subjects: [INFO:INFO_SE] Computer Science/Software Engineering; preuve par récurrence; <br />intégration de modules de raisonnement; <br />verification formelle; <br />procedures de decision; <br />SPIKE
• Online Access: http://tel.archives-ouvertes.fr/tel-00001304; http://tel.archives-ouvertes.fr/docs/00/04/48/29/PDF/tel-00001304.pdf

Le processus de certification de logiciels est dans la plupart des<br /> cas une tâche laborieuse et coûteuse qui nécessite aussi bien des<br /> méthodes mathématiques, pour exprimer sans ambiguïté et de façon<br /> structurée le comportement attendu du logiciel, que des outils<br /> automatiques pour vérifier ses propriétés. Parmi les techniques de<br /> preuve, la récurrence est parfaitement adaptée pour raisonner sur<br /> des structures de données infinies, comme les entiers et les<br /> listes, ou des systèmes paramétrés.<br /> <br /> Cette thèse comprend deux parties, l'une théorique, l'autre<br /> applicative. La première partie est centrée autour d'un nouveau<br /> concept, l'\emph(ensemble couvrant contextuel) (ECC). Le principe<br /> de preuve par récurrence avec ECC est exprimé par un système<br /> d'inférence abstrait qui introduit des conditions suffisantes pour<br /> son application correcte. La conception modulaire de règles<br /> d'inférence concrètes est un avantage de cette approche. Comme<br /> étude de cas, nous spécifions le système d'inférence du<br /> démonstrateur SPIKE en tant qu'instance de ce système.<br /> <br /> Dans la deuxième partie, nous analysons tout d'abord le problème<br /> d'interactions de services téléphoniques. Nous proposons une<br /> méthodologie pour les détecter et les résoudre, reposant sur des<br /> techniques basées sur la réécriture conditionnelle et la<br /> récurrence. Dans une autre application, nous obtenons, à l'aide<br /> du démonstrateur PVS, la première preuve formelle de l'équivalence<br /> entre deux algorithmes de conformité du protocole ABR. Puis,<br /> nous utilisons SPIKE pour vérifier complètement automatiquement<br /> la majorité des 80 lemmes de cette preuve.