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 proceedingConference contributionAcademicpeer-review

1 Citation (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 languageEnglish
Title of host publicationFundamental 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
EditorsHeike Wehrheim, Jordi Cabot
PublisherSpringer Gabler
Pages245-265
Number of pages21
ISBN (Print)9783030452339
DOIs
Publication statusPublished - 2020
Event23rd 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 202030 Apr 2020

Publication series

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

Conference

Conference23rd 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
CountryIreland
CityDublin
Period25/04/2030/04/20

Fingerprint Dive into the research topics of 'Family-Based SPL model checking using parity games with variability'. Together they form a unique fingerprint.

Cite this