Using mCRL2 for the analysis of software product lines

M.H. Beek, ter, E.P. Vink, de

Research output: Book/ReportReportAcademic

298 Downloads (Pure)


We show how the formal specification language mCRL2 and its state-of-the-art toolset can be used successfully to model and analyze variability in software product lines. The mCRL2 toolset supports parametrized modeling, model reduction and quality assurance techniques like model checking. We present a proof-of-concept, which moreover illustrates the use of data in mCRL2 and also how to exploit its data language to manage feature attributes of software product lines and quantitative constraints between attributes and features. Keywords: Model checking, product lines, variability analysis, mCRL2
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages10
Publication statusPublished - 2014

Publication series

NameComputer science reports
ISSN (Print)0926-4515


Dive into the research topics of 'Using mCRL2 for the analysis of software product lines'. Together they form a unique fingerprint.

Cite this