Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Partially Bounded Context-Aware Verification

Luka Le Roux 1 Ciprian Teodorov 1
1 Lab-STICC_ENSTAB_ CACS_MOCS
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
Abstract : Model-checking enables the formal verification of software systems. Powerful and automated, this technique suffers, however, from the state-space explosion problem because of the exponential growth in the number of states with respect to the number of interacting components. To address this problem, the Context-aware Verification (CaV) approach decomposes the verification problem using environment-based guides. This approach improves the scalability but it requires an acyclic specification of the verification guides, which are difficult to specify without losing completeness. In this paper, we present a new verification strategy that generalises CaV while ensuring the decomposability of the state-space. The approach relies on a language for the specification of the arbitrary guides, which relaxes the acyclicity requirement, and on a partially-bounded verification procedure. The effectiveness of our approach is showcased through a case-study from the aerospace domain, which shows that the scalability is maintained while easing the conception of the verification guides.
Keywords : Model checking
Type de document :
Communication dans un congrès
Liste complète des métadonnées

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

https://hal.archives-ouvertes.fr/hal-02434620
Contributeur : Marie Briec <>
Soumis le : mardi 21 avril 2020 - 20:18:39
Dernière modification le : mercredi 24 juin 2020 - 16:19:56

Fichier

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

Identifiants

Citation

Luka Le Roux, Ciprian Teodorov. Partially Bounded Context-Aware Verification. 17th International Conference on Software Engineering and Formal Methods, SEFM 2019, Sep 2019, Oslo, Norway. pp.532-548, ⟨10.1007/978-3-030-30446-1_28⟩. ⟨hal-02434620⟩

Partager

Métriques

Consultations de la notice

96

Téléchargements de fichiers

77