Modeling and Verification for Probabilistic Properties in Software Product Lines

Genaina Nunes Rodrigues; Vander Ramos Alves; NUNES, VINICIUS; André Luiz Peron Martins Lanna; CORDY, MAXIME; YVES; SHARIFLOO, AMIR MOLZAM; LEGAY, AXEL
IEEE 16th International Symposium on High Assurance Systems Engineering (HASE),
View details:  

Abstract

Abstract—We propose a model for feature-aware discrete-time Markov chains, called FDTMC, as a basis for verifying probabilistic properties, e.g., reliability and availability, of product lines. To verify such properties on FDTMC, we compare three techniques. First, we experiment with two different parametric techniques to obtain this formula: the classical one builds it from the model as whole, and a new one that builds it compositionally from a sequence of modules. Finally, we propose a new technique that performs a bounded verification for the whole product line, and thus takes advantage of the high probability of common behaviors of the product line. It computes an approximate formula, represented as an arithmetic decision diagram. Experimental results on a vital signal monitoring system prototype are provided and compared for these techniques aiming at analysing them for scalability issues of size and computational time. They show complementary advantages, and we provide criteria to choose a technique depending on the characteristics of the model.

BibTex references

@inproceedings{DBLP:conf/hase/RodriguesANLCSS15,
  author    = {Gena{\'{\i}}na Nunes Rodrigues and
               Vander Alves and
               Vinicius Nunes and
               Andr{\'{e}} Lanna and
               Maxime Cordy and
               Pierre{-}Yves Schobbens and
               Amir Molzam Sharifloo and
               Axel Legay},
  title     = {Modeling and Verification for Probabilistic Properties in Software
               Product Lines},
  booktitle = {16th {IEEE} International Symposium on High Assurance Systems Engineering,
               {HASE} 2015, Daytona Beach, FL, USA, January 8-10, 2015},
  pages     = {173--180},
  year      = {2015},
  crossref  = {DBLP:conf/hase/2015},
  url       = {http://dx.doi.org/10.1109/HASE.2015.34},
  doi       = {10.1109/HASE.2015.34},
  timestamp = {Fri, 29 Apr 2016 12:29:01 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/hase/RodriguesANLCSS15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/hase/2015,
  title     = {16th {IEEE} International Symposium on High Assurance Systems Engineering,
               {HASE} 2015, Daytona Beach, FL, USA, January 8-10, 2015},
  publisher = {{IEEE} Computer Society},
  year      = {2015},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7027113},
  isbn      = {978-1-4799-8110-6},
  timestamp = {Tue, 16 Jun 2015 19:31:28 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/hase/2015},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

Other publications in the database