Family-based SPL model checking using parity games with variability

DOI10.1007/978-3-030-45234-6_12MaRDI QIDQ5039535zbMATH OpenOpenAlexFDO

Authors Maurice H. ter Beek, Sjef van Loo, Erik de Vink, T. A. C. Willemse

Publication date 13 October 2022

Published in Fundamental Approaches to Software Engineering (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-45234-6_12

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Games involving graphs (91A43) Applications of game theory (91A80)

Recommendations

• Family-based model checking with mCRL2
• Abstract family-based model checking using modal featured transition systems: preservation of \(\mathrm{CTL}^{\star}\)
• Generalized abstraction-refinement for game-based CTL lifted model checking
• Variability-specific abstraction refinement for family-based model checking
• Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints

Cites work

• Abstract family-based model checking using modal featured transition systems: preservation of \(\mathrm{CTL}^{\star}\)
• An overview of the mCRL2 toolset and its recent advances
• Family-based model checking with mCRL2
• Feature integration using a feature construct
• Generalized abstraction-refinement for game-based CTL lifted model checking
• Incremental model checking of delta-oriented software product lines
• Infinite games on finitely coloured graphs with applications to automata on infinite trees
• mCRL2
• Modeling role-based systems with exogenous coordination
• Solving parity games in practice
• The mu-calculus and Model Checking
• Variability-specific abstraction refinement for family-based model checking
• VMC

Cited in

(6)

• Verifying annotated program families using symbolic game semantics
• Generalized abstraction-refinement for game-based CTL lifted model checking
• Model mining and efficient verification of software product lines
• Family-based model checking with mCRL2
• Variability-specific abstraction refinement for family-based model checking
• Featured Team Automata

Describes a project that uses

Uses Software

• mCRL2
• SPIN
• BuDDy
• VMC
• PGSolver
• DeltaCCS

This page was built for publication: Family-based SPL model checking using parity games with variability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5039535)