Proving Partial-Correctness and Invariance Properties of Transition-System Models

Rusu, Vlad; Grimaud, Gilles; Hauspie, Michaël

Type de document :

Communication dans un congrès avec actes

DOI :

10.1109/TASE.2018.00016

Titre :

Proving Partial-Correctness and Invariance Properties of Transition-System Models

Auteur(s) :

Rusu, Vlad [Auteur]
Inria Lille - Nord Europe
Grimaud, Gilles [Auteur]

Université de Lille
Hauspie, Michaël [Auteur]

Université de Lille

Titre de la manifestation scientifique :

TASE 2018 - 12th International Symposium on Theoretical Aspects of Software Engineering

Ville :

Guangzhou

Pays :

Chine

Date de début de la manifestation scientifique :

2018-08-29

Titre de l’ouvrage :

IEEE Xplore

Éditeur :

IEEE Computer Society

Discipline(s) HAL :

Informatique [cs]/Systèmes embarqués
Informatique [cs]/Cryptographie et sécurité [cs.CR]

Résumé en anglais : [en]

We propose a deductive verification approach for proving partial-correctness and invariance properties on transition-system models. Regarding partial correctness, we gen-eralise the recently introduced formalism of ...
Lire la suite >We propose a deductive verification approach for proving partial-correctness and invariance properties on transition-system models. Regarding partial correctness, we gen-eralise the recently introduced formalism of Reachability Logic, currently used as a language-parametric logic for programs, to transition systems. We propose a sound and relatively complete proof system for the resulting reachability logic. The soundness of the proof system is formally established in the Coq proof assistant, and the mechanised proof provides us with a Coq-certified Reachability-Logic prover for transition-system models. The relative completeness of the proof system, although theoretical in nature, also has a practical value, as it induces a proof strategy that is guaranteed to prove all valid formulas on a given transition system. The strategy reduces partial-correctness verification to invariance verification; for the latter we propose an incremental technique in order to deal with the case-explosion problem that affects it. All these techniques were instrumental in enabling us to prove, within reasonable time and effort limits, that the nontrivial algorithm implemented in security hypervisor that we designed in earlier work meets its expected functional requirements.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Collections :

Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL

Fichiers

https://hal.inria.fr/hal-01816798/document
Accès libre
Accéder au document

https://hal.inria.fr/hal-01816798/document
Accès libre
Accéder au document

https://hal.inria.fr/hal-01816798/document
Accès libre
Accéder au document

document
Accès libre
Accéder au document

paper.pdf
Accès libre
Accéder au document

document
Accès libre
Accéder au document

paper.pdf
Accès libre
Accéder au document

Proving Partial-Correctness and Invariance ... BibTeX CSV Excel RIS

Fichiers

Proving Partial-Correctness and Invariance ...

BibTeX

CSV

Excel

RIS