Probabilistic Model Checking for Feature-oriented Systems

Clemens DubslaffClemens Dubslaff, Christel BaierChristel Baier, Sascha KlüppelholzSascha Klüppelholz

DOI Link

Clemens Dubslaff, Christel Baier, Sascha Klüppelholz
Probabilistic Model Checking for Feature-oriented Systems
Transactions on Aspect-Oriented Software Development, 12:180--220, 2015

Details
Bibtex

KurzfassungAbstract
Within product lines, collections of several related products are defined through their commonalities in terms of features rather than specifying them individually one-by-one. In this paper we present a compositional framework for modeling dynamic product lines by a state-based formalism with both probabilistic and nondeterministic behaviors. Rules for feature changes in products made during runtime are formalized by a coordination component imposing constraints on possible feature activations and deactivations. Our framework supports large-scaled product lines described through multi-features, i.e., where products may involve multiple instances of a feature. To establish temporal properties for products in a product line, verification techniques have to face a combinatorial blow-up that arises when reasoning about several feature combinations. This blow-up can be avoided by family-based approaches exploiting common feature behaviors. We adapt such approaches to our framework, allowing for a quantitative analysis in terms of probabilistic model checking to reason, e.g., about energy and memory consumption, monetary costs, or the reliability of products. Our framework can also be used to compute strategies how to trigger feature changes for optimizing quantitative objectives using probabilistic model-checking techniques. We present a natural and conceptually simple translation of product lines into the input language of the prominent probabilistic model checker PRISM and show feasibility of this translation within a case study on an energy-aware server platform product line comprising thousands of products. To cope with the arising complexity, we follow the family-based analysis scheme and apply symbolic methods for a compact state-space representation.
Forschungsgruppe:Research Group: Verifikation und formale quantitative Analyse„Verifikation und formale quantitative Analyse“ befindet sich nicht in der Liste (Computational Logic, Automatentheorie, Wissensverarbeitung, Knowledge-Based Systems, Knowledge Systems, Wissensbasierte Systeme, Logische Programmierung und Argumentation, Algebra und Diskrete Strukturen, Knowledge-aware Artificial Intelligence, Algebraische und logische Grundlagen der Informatik) zulässiger Werte für das Attribut „Forschungsgruppe“.Algebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-46734-3_5.

@article{DBK2015,
  author    = {Clemens Dubslaff and Christel Baier and Sascha Kl{\"{u}}ppelholz},
  title     = {Probabilistic Model Checking for Feature-oriented Systems},
  journal   = {Transactions on Aspect-Oriented Software Development},
  volume    = {12},
  publisher = {Springer},
  year      = {2015},
  pages     = {180--220},
  doi       = {10.1007/978-3-662-46734-3_5}
}