• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 1
  • Tagged with
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
1

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

Stratulat, Sorin 30 November 2000 (has links) (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.

Page generated in 0.1629 seconds