Family-Based SPL model checking using parity games with variability

Maurice H. ter Beek; Sjef van Loo; Erik P. de Vink; Tim A.C. Willemse

doi:10.1007/978-3-030-45234-6_12

Family-Based SPL model checking using parity games with variability

Maurice H. ter Beek, Sjef van Loo, Erik P. de Vink, Tim A.C. Willemse

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

12 Citations (Scopus)

Abstract

Family-based SPL model checking concerns the simultaneous verification of multiple product models, aiming to improve on enumerative product-based verification, by capitalising on the common features and behaviour of products in a software product line (SPL), typically modelled as a featured transition system (FTS). We propose efficient family-based SPL model checking of modal μ-calculus formulae on FTSs based on variability parity games, which extend parity games with conditional edges labelled with feature configurations, by reducing the SPL model checking problem for the modal μ-calculus on FTSs to the variability parity game solving problem, based on an encoding of FTSs as variability parity games. We validate our contribution by experiments on SPL benchmark models, which demonstrate that a novel family-based algorithm to collectively solve variability parity games, using symbolic representations of the configuration sets, outperforms the product-based method of solving the standard parity games obtained by projection with classical algorithms.

Original language	English
Title of host publication	Fundamental Approaches to Software Engineering- 23rd International Conference, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings
Editors	Heike Wehrheim, Jordi Cabot
Publisher	Springer
Pages	245-265
Number of pages	21
ISBN (Print)	9783030452339
DOIs	https://doi.org/10.1007/978-3-030-45234-6_12
Publication status	Published - 2020
Event	23rd International Conference on Fundamental Approaches to Software Engineering, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland Duration: 25 Apr 2020 → 30 Apr 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12076 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	23rd International Conference on Fundamental Approaches to Software Engineering, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
Country/Territory	Ireland
City	Dublin
Period	25/04/20 → 30/04/20

Funding

Acknowledgements Work partially supported by the MIUR PRIN 2017FTXR7S

Access to Document

10.1007/978-3-030-45234-6_12

Cite this

ter Beek, M. H., van Loo, S., de Vink, E. P., & Willemse, T. A. C. (2020). Family-Based SPL model checking using parity games with variability. In H. Wehrheim, & J. Cabot (Eds.), Fundamental Approaches to Software Engineering- 23rd International Conference, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings (pp. 245-265). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12076 LNCS). Springer. https://doi.org/10.1007/978-3-030-45234-6_12

ter Beek, Maurice H. ; van Loo, Sjef ; de Vink, Erik P. et al. / Family-Based SPL model checking using parity games with variability. Fundamental Approaches to Software Engineering- 23rd International Conference, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. editor / Heike Wehrheim ; Jordi Cabot. Springer, 2020. pp. 245-265 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{b3eabcfeb20e4c1ebcd9f5af92500b7b,

title = "Family-Based SPL model checking using parity games with variability",

abstract = "Family-based SPL model checking concerns the simultaneous verification of multiple product models, aiming to improve on enumerative product-based verification, by capitalising on the common features and behaviour of products in a software product line (SPL), typically modelled as a featured transition system (FTS). We propose efficient family-based SPL model checking of modal μ-calculus formulae on FTSs based on variability parity games, which extend parity games with conditional edges labelled with feature configurations, by reducing the SPL model checking problem for the modal μ-calculus on FTSs to the variability parity game solving problem, based on an encoding of FTSs as variability parity games. We validate our contribution by experiments on SPL benchmark models, which demonstrate that a novel family-based algorithm to collectively solve variability parity games, using symbolic representations of the configuration sets, outperforms the product-based method of solving the standard parity games obtained by projection with classical algorithms.",

author = "{ter Beek}, {Maurice H.} and {van Loo}, Sjef and {de Vink}, {Erik P.} and Willemse, {Tim A.C.}",

year = "2020",

doi = "10.1007/978-3-030-45234-6_12",

language = "English",

isbn = "9783030452339",

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

publisher = "Springer",

pages = "245--265",

editor = "Heike Wehrheim and Jordi Cabot",

booktitle = "Fundamental Approaches to Software Engineering- 23rd International Conference, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings",

address = "Germany",

note = "23rd International Conference on Fundamental Approaches to Software Engineering, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 ; Conference date: 25-04-2020 Through 30-04-2020",

}

ter Beek, MH, van Loo, S, de Vink, EP & Willemse, TAC 2020, Family-Based SPL model checking using parity games with variability. in H Wehrheim & J Cabot (eds), Fundamental Approaches to Software Engineering- 23rd International Conference, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12076 LNCS, Springer, pp. 245-265, 23rd International Conference on Fundamental Approaches to Software Engineering, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, 25/04/20. https://doi.org/10.1007/978-3-030-45234-6_12

Family-Based SPL model checking using parity games with variability. / ter Beek, Maurice H.; van Loo, Sjef; de Vink, Erik P. et al.
Fundamental Approaches to Software Engineering- 23rd International Conference, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. ed. / Heike Wehrheim; Jordi Cabot. Springer, 2020. p. 245-265 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12076 LNCS).

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

TY - GEN

T1 - Family-Based SPL model checking using parity games with variability

AU - ter Beek, Maurice H.

AU - van Loo, Sjef

AU - de Vink, Erik P.

AU - Willemse, Tim A.C.

PY - 2020

Y1 - 2020

N2 - Family-based SPL model checking concerns the simultaneous verification of multiple product models, aiming to improve on enumerative product-based verification, by capitalising on the common features and behaviour of products in a software product line (SPL), typically modelled as a featured transition system (FTS). We propose efficient family-based SPL model checking of modal μ-calculus formulae on FTSs based on variability parity games, which extend parity games with conditional edges labelled with feature configurations, by reducing the SPL model checking problem for the modal μ-calculus on FTSs to the variability parity game solving problem, based on an encoding of FTSs as variability parity games. We validate our contribution by experiments on SPL benchmark models, which demonstrate that a novel family-based algorithm to collectively solve variability parity games, using symbolic representations of the configuration sets, outperforms the product-based method of solving the standard parity games obtained by projection with classical algorithms.

AB - Family-based SPL model checking concerns the simultaneous verification of multiple product models, aiming to improve on enumerative product-based verification, by capitalising on the common features and behaviour of products in a software product line (SPL), typically modelled as a featured transition system (FTS). We propose efficient family-based SPL model checking of modal μ-calculus formulae on FTSs based on variability parity games, which extend parity games with conditional edges labelled with feature configurations, by reducing the SPL model checking problem for the modal μ-calculus on FTSs to the variability parity game solving problem, based on an encoding of FTSs as variability parity games. We validate our contribution by experiments on SPL benchmark models, which demonstrate that a novel family-based algorithm to collectively solve variability parity games, using symbolic representations of the configuration sets, outperforms the product-based method of solving the standard parity games obtained by projection with classical algorithms.

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

U2 - 10.1007/978-3-030-45234-6_12

DO - 10.1007/978-3-030-45234-6_12

M3 - Conference contribution

AN - SCOPUS:85084262875

SN - 9783030452339

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

SP - 245

EP - 265

BT - Fundamental Approaches to Software Engineering- 23rd International Conference, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings

A2 - Wehrheim, Heike

A2 - Cabot, Jordi

PB - Springer

T2 - 23rd International Conference on Fundamental Approaches to Software Engineering, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020

Y2 - 25 April 2020 through 30 April 2020

ER -

ter Beek MH, van Loo S, de Vink EP , Willemse TAC. Family-Based SPL model checking using parity games with variability. In Wehrheim H, Cabot J, editors, Fundamental Approaches to Software Engineering- 23rd International Conference, FASE 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. Springer. 2020. p. 245-265. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-45234-6_12

Family-Based SPL model checking using parity games with variability

Abstract

Publication series

Conference

Funding

Access to Document

Other files and links

Fingerprint

Cite this