Family-based model checking with mCRL2

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

21 Citaten (Scopus)
57 Downloads (Pure)

Samenvatting

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.

Originele taal-2Engels
TitelFundamental Approaches to Software Engineering
Subtitel20th 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
RedacteurenM. Huisman, J. Rubin
Plaats van productieDordrecht
UitgeverijSpringer
Pagina's387-405
Aantal pagina's19
ISBN van geprinte versie978-3-662-54494-5
DOI's
StatusGepubliceerd - 2017
Evenement20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017) - Uppsala, Zweden
Duur: 22 apr 201729 apr 2017
Congresnummer: 20
https://www.etaps.org/index.php/2017/fase

Publicatie series

NaamLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10202 LNCS
ISSN van geprinte versie03029743
ISSN van elektronische versie16113349

Congres

Congres20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017)
Verkorte titelFAS#E 2017
LandZweden
StadUppsala
Periode22/04/1729/04/17
Internet adres

Vingerafdruk Duik in de onderzoeksthema's van 'Family-based model checking with mCRL2'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    ter Beek, M. H., de Vink, E. P., & Willemse, T. A. C. (2017). Family-based model checking with mCRL2. In M. Huisman, & J. Rubin (editors), 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 (blz. 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