Family-Based SPL Model Checking Using Parity Games with Variability

DOI10.1007/978-3-030-45234-6_12OpenAlexW3019048927MaRDI QIDQ5039535

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

Publication date: 13 October 2022

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

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

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• mCRL2
• VMC
• Incremental model checking of delta-oriented software product lines
• Infinite games on finitely coloured graphs with applications to automata on infinite trees
• Modeling role-based systems with exogenous coordination
• Generalized abstraction-refinement for game-based CTL lifted model checking
• Abstract family-based model checking using modal featured transition systems: preservation of \(\mathrm{CTL}^{\star}\)
• The mu-calculus and Model Checking
• Solving Parity Games in Practice
• Family-Based Model Checking with mCRL2
• Variability-Specific Abstraction Refinement for Family-Based Model Checking
• An Overview of the mCRL2 Toolset and Its Recent Advances
• Feature integration using a feature construct

This page was built for publication: Family-Based SPL Model Checking Using Parity Games with Variability