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

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

Type de document :

Article dans une revue scientifique: Article original

DOI :

10.1016/j.scico.2019.102342

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 revue :

Science of Computer Programming

Éditeur :

Elsevier

Date de publication :

2020-02-01

ISSN :

0167-6423

Discipline(s) HAL :

Informatique [cs]/Systèmes embarqués
Informatique [cs]/Logique en informatique [cs.LO]

Résumé en anglais : [en]

We propose an approach for proving partial-correctness and invariance properties of transition systems, and illustrate it on a model of a security hypervisor. Regarding partial correctness, we generalise the recently ...
Lire la suite >We propose an approach for proving partial-correctness and invariance properties of transition systems, and illustrate it on a model of a security hypervisor. Regarding partial correctness, we generalise the recently introduced formalism of Reachability Logic, currently used as a language-parametric logic for programs, to transition systems. We propose a coinductive proof system for the resulting logic, which can be seen as performing an “infinite symbolic execution” of the transition-system model under verification. We embed the proof system in the Coq proof assistant and formally prove its soundness and completeness. The soundness result provides us with a Coq-certified Reachability-Logic prover for transition-system models. The completeness result, although more theoretical in nature, also has a practical value, as it suggests a proof strategythat is able to deal with all valid formulas on a given transition system. The complete proof strategy reduces partial correctness to invariance. Forthe latter we propose an incremental verification technique for dealing with the case-explosion problem that is known to affect it. All these combined techniques were instrumental in enabling us to prove, within reasonable time and effort limits, that the nontrivial algorithm implemented in a simple 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-01962912v2/document
Accès libre
Accéder au document

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

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

document
Accès libre
Accéder au document

revision.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