Family-based model checking with mCRL2

DOI10.1007/978-3-662-54494-5_23MaRDI QIDQ5215913zbMATH OpenOpenAlexFDO

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

Publication date 13 February 2020

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

Full work available at URL https://doi.org/10.1007/978-3-662-54494-5_23

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Family-based SPL model checking using parity games with variability
• Abstract family-based model checking using modal featured transition systems: preservation of \(\mathrm{CTL}^{\star}\)
• 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
• From transition systems to variability models and from lifted model checking back to \textsf{UPPAAL}

Cited in

(13)

• Constrained Kripke structure for identifying parameters of biological models
• Family-based SPL model checking using parity games with variability
• A refinement relation for families of timed automata
• Featured Team Automata
• scientific article; zbMATH DE number 7215288 (Why is no real title available?)
• Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints
• Trustworthy variant derivation with translation validation for safety critical product lines
• Verifying annotated program families using symbolic game semantics
• Incremental model checking of delta-oriented software product lines
• Variability-specific abstraction refinement for family-based model checking
• From transition systems to variability models and from lifted model checking back to \textsf{UPPAAL}
• 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}\)

This page was built for publication: Family-based model checking with mCRL2

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