Family-based model checking with mCRL2

M.H. ter Beek; E.P. de Vink; T.A.C. Willemse

doi:10.1007/978-3-662-54494-5_23

Family-based model checking with mCRL2

M.H. ter Beek, E.P. de Vink, T.A.C. Willemse

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

39 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 μL_f, 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	https://doi.org/10.1007/978-3-662-54494-5_23
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	https://www.etaps.org/index.php/2017/fase

Access to Document

10.1007/978-3-662-54494-5_23

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

ter Beek, M.H. ; de Vink, E.P. ; Willemse, T.A.C. / Family-based model checking with mCRL2. 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. editor / M. Huisman ; J. Rubin. Dordrecht : Springer, 2017. pp. 387-405 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{33d378601c4f482789a669a49cb41fcd,

title = "Family-based model checking with mCRL2",

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.",

author = "{ter Beek}, M.H. and {de Vink}, E.P. and T.A.C. Willemse",

year = "2017",

doi = "10.1007/978-3-662-54494-5_23",

language = "English",

isbn = "978-3-662-54494-5",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "387--405",

editor = "M. Huisman and J. Rubin",

booktitle = "Fundamental Approaches to Software Engineering",

address = "Germany",

note = "20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017), FAS#E 2017 ; Conference date: 22-04-2017 Through 29-04-2017",

url = "https://www.etaps.org/index.php/2017/fase",

}

ter Beek, MH, de Vink, EP & Willemse, TAC 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10202 LNCS, Springer, Dordrecht, pp. 387-405, 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017), Uppsala, Sweden, 22/04/17. https://doi.org/10.1007/978-3-662-54494-5_23

Family-based model checking with mCRL2. / ter Beek, M.H.; de Vink, E.P.; Willemse, T.A.C.
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. ed. / M. Huisman; J. Rubin. Dordrecht: Springer, 2017. p. 387-405 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10202 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Family-based model checking with mCRL2

AU - ter Beek, M.H.

AU - de Vink, E.P.

AU - Willemse, T.A.C.

N1 - Conference code: 20

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85016429689&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-54494-5_23

DO - 10.1007/978-3-662-54494-5_23

M3 - Conference contribution

AN - SCOPUS:85016429689

SN - 978-3-662-54494-5

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 387

EP - 405

BT - Fundamental Approaches to Software Engineering

A2 - Huisman, M.

A2 - Rubin, J.

PB - Springer

CY - Dordrecht

T2 - 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017)

Y2 - 22 April 2017 through 29 April 2017

ER -

ter Beek MH, de Vink EP , Willemse TAC. Family-based model checking with mCRL2. In Huisman M, Rubin J, 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. Dordrecht: Springer. 2017. p. 387-405. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-54494-5_23

Family-based model checking with mCRL2

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this