Family-based model checking of SPL based on mCRL2

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

We discuss how the general-purpose model checker mCRL2 can be used for family-based verification of behavioral properties of software product lines. This is achieved by exploiting a featureoriented extension of the modal μ-calculus for the specification of SPL properties, and for its model checking by encoding it back into the logic of mCRL2. Using the example of the well-known minepump SPL an illustration of the possibilities of the approach is given.

Original languageEnglish
Title of host publicationSPLC '17 Proceedings of the 21st International Systems and Software Product Line Conference, 25-29 September 2017, Sevilla, Spain
Place of PublicationNew York
PublisherAssociation for Computing Machinery, Inc
Pages13-16
Number of pages4
VolumeB
ISBN (Print)978-1-4503-5119-5
DOIs
Publication statusPublished - 25 Sept 2017
Event21st International Systems and Software Product Line Conference (SPLC 2017) - Sevilla, Spain
Duration: 25 Sept 201729 Sept 2017
Conference number: 21

Conference

Conference21st International Systems and Software Product Line Conference (SPLC 2017)
Abbreviated titleSPLC 2017
Country/TerritorySpain
CitySevilla
Period25/09/1729/09/17

Keywords

  • Family-based model checking
  • MCRL2
  • Software product lines

Fingerprint

Dive into the research topics of 'Family-based model checking of SPL based on mCRL2'. Together they form a unique fingerprint.

Cite this