A Logic for the Statistical Model Checking of Dynamic Software Architectures

Jean Quilbeuf 1, 2 Everton Cavalcante 2, 3 Louis-Marie Traonouez 1 Flavio Oquendo 2 Thais Batista 3 Axel Legay 1
1 TAMIS - Threat Analysis and Mitigation for Information Security
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 ArchWare
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires
Abstract : Dynamic software architectures emerge when addressing important features of contemporary systems, which often operate in dynamic environments subjected to change. Such systems are designed to be reconfigured over time while maintaining important properties, e.g., availability, correctness, etc. Verifying that reconfiguration operations make the system to meet the desired properties remains a major challenge. First, the verification process itself becomes often difficult when using exhaustive formal methods (such as model checking) due to the potentially infinite state space. Second, it is necessary to express the properties to be verified using some notation able to cope with the dynamic nature of these systems. Aiming at tackling these issues, we introduce DynBLTL, a new logic tailored to express both structural and behavioral properties in dynamic software architectures. Furthermore, we propose using statistical model checking (SMC) to support an efficient analysis of these properties by evaluating the probability of meeting them through a number of simulations. In this paper, we describe the main features of DynBLTL and how it was implemented as a plug-in for PLASMA, a statistical model checker.
Type de document :
Communication dans un congrès
ISoLA, Oct 2016, Corfou, Greece. Springer, 9952, pp.806 - 820, 2016, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 〈10.1007/978-3-319-47166-2_56〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01387429
Contributeur : Louis-Marie Traonouez <>
Soumis le : mardi 25 octobre 2016 - 15:26:08
Dernière modification le : mercredi 16 mai 2018 - 11:24:11

Fichier

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

Identifiants

Citation

Jean Quilbeuf, Everton Cavalcante, Louis-Marie Traonouez, Flavio Oquendo, Thais Batista, et al.. A Logic for the Statistical Model Checking of Dynamic Software Architectures. ISoLA, Oct 2016, Corfou, Greece. Springer, 9952, pp.806 - 820, 2016, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 〈10.1007/978-3-319-47166-2_56〉. 〈hal-01387429〉

Partager

Métriques

Consultations de la notice

594

Téléchargements de fichiers

157