Towards modular verification of software product lines with mCRL2

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

doi:10.1007/978-3-662-45234-9_26

Towards modular verification of software product lines with mCRL2

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

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

20 Citations (Scopus)

4 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 language	English
Title of host publication	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)
Editors	T. Margaria, B. Steffen
Place of Publication	Berlin
Publisher	Springer
Pages	368-385
ISBN (Print)	978-3-662-45233-2
DOIs	https://doi.org/10.1007/978-3-662-45234-9_26
Publication status	Published - 2014
Event	6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2014) - Corfu, Greece Duration: 8 Oct 2014 → 11 Oct 2014 Conference number: 6

Publication series

Name	Lecture Notes in Computer Science
Volume	8802
ISSN (Print)	0302-9743

Conference

Conference	6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2014)
Abbreviated title	ISoLA 2014
Country/Territory	Greece
City	Corfu
Period	8/10/14 → 11/10/14

Access to Document

10.1007/978-3-662-45234-9_26

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

Beek, ter, M.H. ; Vink, de, E.P. / Towards modular verification of software product lines with mCRL2. 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). editor / T. Margaria ; B. Steffen. Berlin : Springer, 2014. pp. 368-385 (Lecture Notes in Computer Science).

@inproceedings{95954a916f61449e80623bbb3b8656b7,

title = "Towards modular verification of software product lines with mCRL2",

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.",

author = "{Beek, ter}, M.H. and {Vink, de}, E.P.",

year = "2014",

doi = "10.1007/978-3-662-45234-9_26",

language = "English",

isbn = "978-3-662-45233-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "368--385",

editor = "T. Margaria and B. Steffen",

booktitle = "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)",

address = "Germany",

note = "6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2014), ISoLA 2014 ; Conference date: 08-10-2014 Through 11-10-2014",

}

Beek, ter, MH & Vink, de, EP 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). Lecture Notes in Computer Science, vol. 8802, Springer, Berlin, pp. 368-385, 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2014), Corfu, Greece, 8/10/14. https://doi.org/10.1007/978-3-662-45234-9_26

Towards modular verification of software product lines with mCRL2. / Beek, ter, M.H.; Vink, de, E.P.
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). ed. / T. Margaria; B. Steffen. Berlin: Springer, 2014. p. 368-385 (Lecture Notes in Computer Science; Vol. 8802).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Towards modular verification of software product lines with mCRL2

AU - Beek, ter, M.H.

AU - Vink, de, E.P.

N1 - Conference code: 6

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-662-45234-9_26

DO - 10.1007/978-3-662-45234-9_26

M3 - Conference contribution

SN - 978-3-662-45233-2

T3 - Lecture Notes in Computer Science

SP - 368

EP - 385

BT - 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)

A2 - Margaria, T.

A2 - Steffen, B.

PB - Springer

CY - Berlin

T2 - 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2014)

Y2 - 8 October 2014 through 11 October 2014

ER -

Beek, ter MH, Vink, de EP. Towards modular verification of software product lines with mCRL2. In Margaria T, Steffen B, editors, 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). Berlin: Springer. 2014. p. 368-385. (Lecture Notes in Computer Science). doi: 10.1007/978-3-662-45234-9_26

Towards modular verification of software product lines with mCRL2

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this