Cargando…
Family-Based SPL Model Checking Using Parity Games with Variability
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 transiti...
Autores principales: | , , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7418119/ http://dx.doi.org/10.1007/978-3-030-45234-6_12 |
_version_ | 1783569629344432128 |
---|---|
author | ter Beek, Maurice H. van Loo, Sjef de Vink, Erik P. Willemse, Tim A. C. |
author_facet | ter Beek, Maurice H. van Loo, Sjef de Vink, Erik P. Willemse, Tim A. C. |
author_sort | ter Beek, Maurice H. |
collection | PubMed |
description | 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 [Formula: see text]-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 [Formula: see text]-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. |
format | Online Article Text |
id | pubmed-7418119 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
record_format | MEDLINE/PubMed |
spelling | pubmed-74181192020-08-11 Family-Based SPL Model Checking Using Parity Games with Variability ter Beek, Maurice H. van Loo, Sjef de Vink, Erik P. Willemse, Tim A. C. Fundamental Approaches to Software Engineering Article 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 [Formula: see text]-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 [Formula: see text]-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. 2020-03-13 /pmc/articles/PMC7418119/ http://dx.doi.org/10.1007/978-3-030-45234-6_12 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. |
spellingShingle | Article ter Beek, Maurice H. van Loo, Sjef de Vink, Erik P. Willemse, Tim A. C. Family-Based SPL Model Checking Using Parity Games with Variability |
title | Family-Based SPL Model Checking Using Parity Games with Variability |
title_full | Family-Based SPL Model Checking Using Parity Games with Variability |
title_fullStr | Family-Based SPL Model Checking Using Parity Games with Variability |
title_full_unstemmed | Family-Based SPL Model Checking Using Parity Games with Variability |
title_short | Family-Based SPL Model Checking Using Parity Games with Variability |
title_sort | family-based spl model checking using parity games with variability |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7418119/ http://dx.doi.org/10.1007/978-3-030-45234-6_12 |
work_keys_str_mv | AT terbeekmauriceh familybasedsplmodelcheckingusingparitygameswithvariability AT vanloosjef familybasedsplmodelcheckingusingparitygameswithvariability AT devinkerikp familybasedsplmodelcheckingusingparitygameswithvariability AT willemsetimac familybasedsplmodelcheckingusingparitygameswithvariability |