Family-based model checking with mCRL2

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

21 Citations (Scopus)
57 Downloads (Pure)

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 languageEnglish
Title of host publicationFundamental Approaches to Software Engineering
Subtitle of host publication20th 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
EditorsM. Huisman, J. Rubin
Place of PublicationDordrecht
PublisherSpringer
Pages387-405
Number of pages19
ISBN (Print)978-3-662-54494-5
DOIs
Publication statusPublished - 2017
Event20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017) - Uppsala, Sweden
Duration: 22 Apr 201729 Apr 2017
Conference number: 20
https://www.etaps.org/index.php/2017/fase

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10202 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017)
Abbreviated titleFAS#E 2017
CountrySweden
CityUppsala
Period22/04/1729/04/17
OtherHeld as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
Internet address

Fingerprint Dive into the research topics of 'Family-based model checking with mCRL2'. Together they form a unique fingerprint.

  • Cite this

    ter Beek, M. H., de Vink, E. P., & Willemse, T. A. C. (2017). Family-based model checking with mCRL2. In M. Huisman, & J. Rubin (Eds.), Fundamental Approaches to Software Engineering: 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 (pp. 387-405). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10202 LNCS). Springer. https://doi.org/10.1007/978-3-662-54494-5_23