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