Towards modular verification of software product lines with mCRL2

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

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

14 Citations (Scopus)
3 Downloads (Pure)

Abstract

We introduce by means of an example a modular verification technique for analyzing the behavior of software product lines using the mCRL2 toolset. Based on feature-driven borders, we divide a behavioral model of a product line into a set of separate components with interfaces and a driver process to coordinate them. Abstracting from irrelevant components, we verify properties over a smaller behavioral model, which not only simplifies the model checking task but also makes the result amenable for reuse. This is a fundamental step forward for the approach to scale up to industrial-size product lines.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change (6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part I)
EditorsT. Margaria, B. Steffen
Place of PublicationBerlin
PublisherSpringer
Pages368-385
ISBN (Print)978-3-662-45233-2
DOIs
Publication statusPublished - 2014
Event6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2014) - Corfu, Greece
Duration: 8 Oct 201411 Oct 2014
Conference number: 6

Publication series

NameLecture Notes in Computer Science
Volume8802
ISSN (Print)0302-9743

Conference

Conference6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2014)
Abbreviated titleISoLA 2014
CountryGreece
CityCorfu
Period8/10/1411/10/14

Fingerprint Dive into the research topics of 'Towards modular verification of software product lines with mCRL2'. Together they form a unique fingerprint.

  • Cite this

    Beek, ter, M. H., & Vink, de, E. P. (2014). Towards modular verification of software product lines with mCRL2. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change (6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part I) (pp. 368-385). (Lecture Notes in Computer Science; Vol. 8802). Springer. https://doi.org/10.1007/978-3-662-45234-9_26