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

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

Samenvatting

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.

Originele taal-2	Engels
Titel	SPLC '17 Proceedings of the 21st International Systems and Software Product Line Conference, 25-29 September 2017, Sevilla, Spain
Plaats van productie	New York
Uitgeverij	Association for Computing Machinery, Inc
Pagina's	13-16
Aantal pagina's	4
Volume	B
ISBN van geprinte versie	978-1-4503-5119-5
DOI's	https://doi.org/10.1145/3109729.3109758
Status	Gepubliceerd - 25 sep. 2017
Evenement	21st International Systems and Software Product Line Conference (SPLC 2017) - Sevilla, Spanje Duur: 25 sep. 2017 → 29 sep. 2017 Congresnummer: 21

Congres

Congres	21st International Systems and Software Product Line Conference (SPLC 2017)
Verkorte titel	SPLC 2017
Land/Regio	Spanje
Stad	Sevilla
Periode	25/09/17 → 29/09/17

Toegang tot document

10.1145/3109729.3109758

Andere bestanden en links

Link to publication in Scopus

Citeer dit

@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, blz. 13-16, 21st International Systems and Software Product Line Conference (SPLC 2017), Sevilla, Spanje, 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. blz. 13-16.

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › 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 - http://www.scopus.com/inward/record.url?scp=85032285859&partnerID=8YFLogxK

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

Samenvatting

Congres

Toegang tot document

Andere bestanden en links

Vingerafdruk

Citeer dit