Paper Info
Title
A Logic for the Statistical Model Checking of Dynamic Software Architectures.
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.
Year
DOI
Venue
2016
10.1007/978-3-319-47166-2_56
Lecture Notes in Computer Science
Field
DocType
Volume
Notation,Model checking,Programming language,Computer science,Correctness,Theoretical computer science,Software,Statistical model,Formal methods,State space,Control reconfiguration
Conference
9952
ISSN
Citations 
PageRank 
0302-9743
8
0.52
References 
Authors
17
6
Name
Order
Citations
PageRank
Jean Quilbeuf113812.10
Everton Cavalcante214124.32
Louis-Marie Traonouez324318.50
Flávio Oquendo436387.03
Thais Batista547444.46
Axel Legay62982181.47