RPP : Preuve automatique de propriétés relationnelles par Self-Composition

Résumé : Contexte. Les méthodes de vérification déductive basées sur la logique de Hoare [7] fournissent une approche puissante pour prouver qu'une fonction respecte certaines propriétés. Elles sont généralement couplées à un langage permettant de spécifier formellement les propriétés attendues, en particulier sous forme de contrats de fonction. Un tel contrat comprend des pré-et des post-conditions décrivant respectivement les entrées attendues et le comportement exigé de la fonction. Problème. Cependant, toutes les propriétés qu'on peut vouloir établir sur un programme donné ne s'expriment pas facilement sous cette forme. En effet, un contrat de fonction décrit le déroulement d'une exécution d'une fonction donnée. Cependant, il est fréquent qu'on veuille parler d'une propriété relationnelle mettant en jeu l'exécution de plusieurs fonctions, ou comparer les résultats d'une même fonction sur différents paramètres. En particulier, des groupes de fonctions sont fréquemment liés par des spécifications algébriques [8] précisant leurs relations. Les contrats de fonction et les méthodes déductives classiques se prêtent mal à la spécification et à la vérification de telles propriétés. Des exemples de telles propriétés incluent : ∀x, y; x <= y => f (x) <= f (y) Decrypt(Crypt(M sg, P rivKey), P ubKey) = M sg On retrouve un sous ensemble des propriétés relationnelles dans le domaine du test, appelées propriétés métamorphique [6], liant plusieurs appels de la même fonction. Contributions. Afin de répondre a ce manque de support pour les propriétés relationnelles lors de la vérification à base de contrats, nous proposons le plugin FRAMA-C/RPP présenté dans [4]. L'outil réalise un ensemble de transformations automatiques à partir d'un langage de spécification capable d'exprimer des propriétés relationnelles. Le résultat des transformations permet de prouver des propriétés relationnelles et de les utiliser comme hypothèse dans d'autres preuves en utilisant des outils de vérification déductive standard.
Document type :
Conference papers
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01835491
Contributor : Virgile Prevosto <>
Submitted on : Wednesday, July 11, 2018 - 2:05:53 PM
Last modification on : Thursday, February 7, 2019 - 4:50:52 PM
Long-term archiving on : Saturday, October 13, 2018 - 2:00:34 AM

File

rpp.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-01835491, version 1

Citation

Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prévosto. RPP : Preuve automatique de propriétés relationnelles par Self-Composition. Approches Formelles pour l'Assistance au Développement de Logiciels - AFADL, Jun 2018, Grenoble, France. ⟨cea-01835491⟩

Share

Metrics

Record views

266

Files downloads

42