Family-based model checking of SPL based on mCRL2

Z.B. Snaiba; E.P. de Vink; T.A.C. Willemse

doi:10.1145/3109729.3109758

Family-based model checking of SPL based on mCRL2

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	SPLC '17 Proceedings of the 21st International Systems and Software Product Line Conference, 25-29 September 2017, Sevilla, Spain
Place of Publication	New York
Publisher	Association for Computing Machinery, Inc.
Pages	13-16
Number of pages	4
Volume	B
ISBN (Print)	978-1-4503-5119-5
DOIs	https://doi.org/10.1145/3109729.3109758
Publication status	Published - 25 Sept 2017
Event	21st International Systems and Software Product Line Conference (SPLC 2017) - Sevilla, Spain Duration: 25 Sept 2017 → 29 Sept 2017 Conference number: 21

Conference

Conference	21st International Systems and Software Product Line Conference (SPLC 2017)
Abbreviated title	SPLC 2017
Country/Territory	Spain
City	Sevilla
Period	25/09/17 → 29/09/17

Keywords

Family-based model checking
MCRL2
Software product lines

Access to Document

10.1145/3109729.3109758

Cite this

@inproceedings{2bed6cd786894a8eada3f2eb2d84dbc7,

title = "Family-based model checking of SPL based on mCRL2",

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

keywords = "Family-based model checking, MCRL2, Software product lines",

author = "Z.B. Snaiba and \{de Vink\}, E.P. and T.A.C. Willemse",

year = "2017",

month = sep,

day = "25",

doi = "10.1145/3109729.3109758",

language = "English",

isbn = "978-1-4503-5119-5 ",

volume = "B",

pages = "13--16",

booktitle = "SPLC '17 Proceedings of the 21st International Systems and Software Product Line Conference, 25-29 September 2017, Sevilla, Spain",

publisher = "Association for Computing Machinery, Inc.",

address = "United States",

note = "21st International Systems and Software Product Line Conference (SPLC 2017), SPLC 2017 ; Conference date: 25-09-2017 Through 29-09-2017",

}

Snaiba, ZB, de Vink, EP & Willemse, TAC 2017, Family-based model checking of SPL based on mCRL2. in SPLC '17 Proceedings of the 21st International Systems and Software Product Line Conference, 25-29 September 2017, Sevilla, Spain. vol. B, Association for Computing Machinery, Inc., New York, pp. 13-16, 21st International Systems and Software Product Line Conference (SPLC 2017), Sevilla, Spain, 25/09/17. https://doi.org/10.1145/3109729.3109758

Family-based model checking of SPL based on mCRL2. / Snaiba, Z.B.; de Vink, E.P.; Willemse, T.A.C.
SPLC '17 Proceedings of the 21st International Systems and Software Product Line Conference, 25-29 September 2017, Sevilla, Spain. Vol. B New York: Association for Computing Machinery, Inc., 2017. p. 13-16.

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

TY - GEN

T1 - Family-based model checking of SPL based on mCRL2

AU - Snaiba, Z.B.

AU - de Vink, E.P.

AU - Willemse, T.A.C.

N1 - Conference code: 21

PY - 2017/9/25

Y1 - 2017/9/25

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

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

KW - Family-based model checking

KW - MCRL2

KW - Software product lines

UR - https://www.scopus.com/pages/publications/85032285859

U2 - 10.1145/3109729.3109758

DO - 10.1145/3109729.3109758

M3 - Conference contribution

AN - SCOPUS:85032285859

SN - 978-1-4503-5119-5

VL - B

SP - 13

EP - 16

BT - SPLC '17 Proceedings of the 21st International Systems and Software Product Line Conference, 25-29 September 2017, Sevilla, Spain

PB - Association for Computing Machinery, Inc.

CY - New York

T2 - 21st International Systems and Software Product Line Conference (SPLC 2017)

Y2 - 25 September 2017 through 29 September 2017

ER -

Family-based model checking of SPL based on mCRL2

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this