Mechanical Verification of Interactive Programs Specified by Use Cases

Guillaume Claret 1 Yann Régis-Gianas 1
1 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : Interactive programs, like user interfaces, are hard to formally specify and thus to prove correct. Some ideas coming from functional programming languages have been successful to improve the way we write safer programs, compared to traditional imperative languages, but these ideas mostly apply to code fragments without any inputs–outputs. Using the purely functional language Coq, we present a new technique to represent interactive programs and formally verify use cases using the Coq proof engine as a symbolic debugger. To this end we introduce the notion of scenarios, well-typed schema of interactions between an environment and a program. We design and certify a blog system as an illustration. Our approach generalizes unit-testing techniques and outlines a new method for mechanically assisted checking of effectful functional programs. I. Introduction Implementing and proving correct interactive programs is challenging. Indeed, interactive programs are hard to reason about because they communicate with an outer environment (the operating system, the network, the user,. . .) which may be under-specified and non determin-istic. Moreover, the communications between the program and the environment can happen at many points during the execution and may depend on previous interactions. Many techniques have been developed to model, specify and prove correct interactive or concurrent programs[15]. For instance, process algebra and temporal logics are well understood abstract models for such programs. In these abstract models, some interesting behavioral properties can be automatically proved by model-checkers. Yet, these tools usually provide guarantees about the model of the program, not its actual implementation. In another approach, called software-proof co-design, the specification and the verification of a program is not disconnected from its actual implementation. In that case, specifying, implementing and verifying are tightly interleaved in the software development process. This tight integration is possible within the Coq proof assistant which is both a programming language and an assisted prover. Yet, even if a realistic compiler for the C language has already been developed in Coq[12], using Coq as a general purpose programming language may be considered
Type de document :
Communication dans un congrès
3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, May 2015, Florence, Italy. 2015, 〈10.1109/FormaliSE.2015.17〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01255107
Contributeur : Yann Regis-Gianas <>
Soumis le : mercredi 13 janvier 2016 - 10:58:03
Dernière modification le : mercredi 30 mai 2018 - 09:55:03
Document(s) archivé(s) le : vendredi 11 novembre 2016 - 03:41:02

Fichier

index.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | PPS | USPC

Citation

Guillaume Claret, Yann Régis-Gianas. Mechanical Verification of Interactive Programs Specified by Use Cases. 3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, May 2015, Florence, Italy. 2015, 〈10.1109/FormaliSE.2015.17〉. 〈hal-01255107〉

Partager

Métriques

Consultations de la notice

283

Téléchargements de fichiers

169