Modeling and Verification for Probabilistic Properties in Software Product Lines

Genaina N. Rodrigues, Vander Alves, Vinicius Nunes, Andre Lanna, Maxime Cordy, Pierre Yves Schobbens, Amir Molzam Sharifloo, Axel Legay

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publicationProceedings of IEEE International Symposium on High Assurance Systems Engineering
PublisherIEEE Computer Society Press
Pages173-180
Number of pages8
Volume2015
EditionJanuary
DOIs
Publication statusPublished - 29 Jan 2015
Event16th IEEE International Symposium on High Assurance Systems Engineering, HASE 2015 - Daytona Beach, United States
Duration: 8 Jan 201510 Jan 2015

Conference

Conference16th IEEE International Symposium on High Assurance Systems Engineering, HASE 2015
CountryUnited States
CityDaytona Beach
Period8/01/1510/01/15

Keywords

  • DTMC
  • parametric model checking
  • probabilistic verification
  • Software Product Lines

Fingerprint Dive into the research topics of 'Modeling and Verification for Probabilistic Properties in Software Product Lines'. Together they form a unique fingerprint.

Cite this