Statistical Model Checking of Dynamic Software Architectures

Everton Cavalcante 1, 2 Jean Quilbeuf 3, 1 Louis-Marie Traonouez 3 Flavio Oquendo 1 Thais Batista 2 Axel Legay 3
1 ArchWare
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires
3 TAMIS - Threat Analysis and Mitigation for Information Security
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The critical nature of many complex software-intensive systems calls for formal, rigorous architecture descriptions as means of supporting automated verification and enforcement of architectural properties and constraints. Model checking has been one of the most used techniques to automatically analyze software architectures with respect to the satisfaction of architectural properties. However, such a technique leads to an exhaustive exploration of all possible states of the system under verification, a problem that becomes more severe when verifying dynamic software systems due to their typical non-deterministic runtime behavior and unpredictable operation conditions. To tackle these issues, we propose using statistical model checking (SMC) to support the analysis of dynamic software architectures while aiming at reducing effort, computational resources, and time required for this task. In this paper, we introduce a novel notation to formally express architectural properties as well as an SMC-based toolchain for verifying dynamic software architectures described in π-ADL, a formal architecture description language. We use a flood monitoring system to show how to express relevant properties to be verified, as well as we report the results of some computational experiments performed to assess the efficiency of our approach.
Type de document :
Communication dans un congrès
ECSA 2016 - 10th European Conference on Software Architecture, Nov 2016, Copenhague, Denmark. Proceedings of the 2016 European Conference of Software Architecture, Proceedings of the 2016 European Conference of Software Architecture
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01390707
Contributeur : Jean Quilbeuf <>
Soumis le : lundi 7 novembre 2016 - 12:57:12
Dernière modification le : vendredi 16 novembre 2018 - 01:37:25
Document(s) archivé(s) le : mercredi 8 février 2017 - 14:05:52

Fichier

2016-ECSA.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01390707, version 1

Citation

Everton Cavalcante, Jean Quilbeuf, Louis-Marie Traonouez, Flavio Oquendo, Thais Batista, et al.. Statistical Model Checking of Dynamic Software Architectures. ECSA 2016 - 10th European Conference on Software Architecture, Nov 2016, Copenhague, Denmark. Proceedings of the 2016 European Conference of Software Architecture, Proceedings of the 2016 European Conference of Software Architecture. 〈hal-01390707〉

Partager

Métriques

Consultations de la notice

820

Téléchargements de fichiers

238