Abstract
Family-based model checking targets the simultaneous verfication of multiple system variants, a technique to handle feature-based variability that is intrinsic to software product lines (SPLs). We present an approach for family-based verification based on the feature μ-calculus μLf, which combines modalities with feature expressions. This logic is interpreted over featured transition systems, a well-accepted model of SPLs, which allows one to reason over the collective behavior of a number of variants (a family of products). Via an embedding into the modal μ-calculus with data, underpinned by the general-purpose mCRL2 toolset, off-the-shelf tool support for μLf becomes readily available. We illustrate the feasibility of our approach on an SPL benchmark model and show the runtime improvement that family-based model checking with mCRL2 offers with respect to model checking the benchmark product-by-product.
Original language | English |
---|---|
Title of host publication | Fundamental Approaches to Software Engineering |
Subtitle of host publication | 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings |
Editors | M. Huisman, J. Rubin |
Place of Publication | Dordrecht |
Publisher | Springer |
Pages | 387-405 |
Number of pages | 19 |
ISBN (Print) | 978-3-662-54494-5 |
DOIs | |
Publication status | Published - 2017 |
Event | 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017) - Uppsala, Sweden Duration: 22 Apr 2017 → 29 Apr 2017 Conference number: 20 https://www.etaps.org/index.php/2017/fase |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 10202 LNCS |
ISSN (Print) | 03029743 |
ISSN (Electronic) | 16113349 |
Conference
Conference | 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017) |
---|---|
Abbreviated title | FAS#E 2017 |
Country/Territory | Sweden |
City | Uppsala |
Period | 22/04/17 → 29/04/17 |
Other | Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 |
Internet address |