short-paper

Family-Based Model Checking of SPL based on mCRL2

Authors:

Ziad Ben Snaiba,

Erik P. de Vink,

Tim A.C. WillemseAuthors Info & Claims

SPLC '17: Proceedings of the 21st International Systems and Software Product Line Conference - Volume B

Pages 13 - 16

https://doi.org/10.1145/3109729.3109758

Published: 25 September 2017 Publication History

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 feature-oriented 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.

References

[1]

J.M. Atlee, S. Beidu, N.A. Day, F. Faghih, and P. Shaker. 2013. Recommendations for improving the usability of formal methods for product lines. In FormaliSE 2013, San Francisco. IEEE Computer Society, 43--49. https://doi.org/10.1109/FormaliSE.2013.6612276

[2]

M.H. ter Beek, A. Fantechi, S. Gnesi, and M. Mazzanti. 2015. Using FMC for Family-Based Analysis of Software Product Lines. In Proc. SPLC, D. Schmidt (Ed.). ACM, 432--439. https://doi.org/10.1145/2791060.2791118

Digital Library

[3]

M.H. ter Beek and E.P. de Vink. 2014. Using mCRL2 for the analysis of software product lines. In FormaliSE workshop at ICSE'14, S. Gnesi and N. Plat (Eds.). IEEE, 31--37. https://doi.org/10.1145/2593489.2593493

[4]

M.H. ter Beek, E.P. de Vink, and T.A.C. Willemse. 2016. Towards a feature mucalculus targeting SPL verification. In Proc. FMSPLE 2016, J. Rubin and T. Thuem (Eds.). EPTCS, 15pp. https://doi.org/10.4204/EPTCS.206.6

[5]

M.H. ter Beek, E.P. de Vink, and T.A.C. Willemse. 2017. Family-Based Model Checking with mCRL2. In Proc. FASE 2017, M. Huisman and J. Rubin (Eds.). LNCS 10202, 387--405. https://doi.org/10.1007/978-3-662-54494-5_23

[6]

P. Borba, M.B. Cohen, A. Legay, and A. Wasowski. 2013. Analysis, Test and Verification in The Presence of Variability (Dagstuhl Seminar 13091). Dagstuhl Reports 3, 2 (2013), 144--170. https://doi.org/10.4230/DagRep.3.2.144

[7]

J. Bradfield and C. Stirling. 2006. Modal mu-calculi. In The Handbook of Modal Logic, P. Blackburn, J. van Benthem, and F. Wolter (Eds.). Elsevier, 721--756.

[8]

E.M. Clarke, E.A. Emerson, and J. Sifakis. 2009. Model checking: algorithmic verification and debugging. Commun. ACM 52, 11 (2009), 74--84. https://doi.org/10.1145/1592761.1592781

Digital Library

[9]

A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens. 2014. Formal Semantics, modular specification, and symbolic verification of product-line behaviour. Science of Computer Programming 80, B (2014), 416--439. https://doi.org/10.1145/2499777.2499781

[10]

A. Classen, M. Cordy, P.-Y. Schobbens, P. Heymans, A. Legay, and J.-F. Raskin. 2013. Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE Trans. Software Eng. 39, 8 (2013), 1069--1089. https://doi.org/10.1109/TSE.2012.86

Digital Library

[11]

A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. 2011. Symbolic model checking of software product lines. In Proc. ICSE 2011, Honolulu. IEEE, 321--330. https://doi.org/10.1145/1985793.1985838

Digital Library

[12]

A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay, and J.-F. Raskin. 2010. Model checking lots of systems: efficient verification of temporal properties in software product lines. In Proc. ICSE 2010. 335--344. https://doi.org/10.1145/1806799.1806850

Digital Library

[13]

M. Cordy, A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. 2013. ProVeLines: a product line of verifiers for software product lines. In Proc. SPLC 2013, Tokyo. ACM, 141--146. https://doi.org/10.1145/2499777.2499781

Digital Library

[14]

S. Cranen, J.F. Groote, J.J.A. Keiren, F.P.M. Stappers, E.P. de Vink, W. Wesselink, and T.A.C. Willemse. 2013. An Overview of the mCRL2 Toolset and Its Recent Advances. In Proc. TACAS 2013, N. Piterman and S.A. Smolka (Eds.). LNCS 7795, 199--213. https://doi.org/10.1007/978-3-642-36742-7_15

Digital Library

[15]

A.S. Dimovski and A. Wasowski. 2017. Variability-Specific Abstraction Refinement for Family-Based Model Checking. In Proc. FASE 2017, M. Huisman and J. Rubin (Eds.). LNCS 10202, 406--423. https://doi.org/10.1007/978-3-662-54494-5_24

[16]

J. Kramer, J. Magee, M. Sloman, and A. Lister. 1983. CONIC: an integrated approach to distributed computer control systems. IEE Proc. E 130, 1 (1983), 1--10. https://doi.org/10.1049/ip-e.1983.0001

[17]

T. Parr. 2012. The definitive ANTLR 4 reference. The Pragmatic Programmer.

[18]

I. Schaefer and R. Hähnle. 2011. Formal Methods in Software Product Line Engineering. IEEE Computer 44, 2 (2011), 82--85. https://doi.org/10.1109/MC.2011.47

Digital Library

Cited By

Kishi T(2023)Family-based Model Checking using Probabilistic Model Checker PRISM2023 30th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC60848.2023.00048(376-385)Online publication date: 4-Dec-2023
https://doi.org/10.1109/APSEC60848.2023.00048
Bunte OGroote JKeiren JLaveaux MNeele Tde Vink EWesselink WWijs AWillemse T(2019)The mCRL2 Toolset for Analysing Concurrent SystemsAdvances in Knowledge Discovery and Data Mining10.1007/978-3-030-17465-1_2(21-39)Online publication date: 3-Apr-2019
https://doi.org/10.1007/978-3-030-17465-1_2

Index Terms

Family-Based Model Checking of SPL based on mCRL2
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
      1. Reusability
        Software product lines
2. Theory of computation
  1. Logic
    1. Logic and verification
    2. Verification by model checking

Recommendations

Efficient family-based model checking via variability abstractions

Many software systems are variational: they can be configured to meet diverse sets of requirements. They can produce a (potentially huge) number of related systems, known as products or variants, by systematically reusing common parts. For variational ...
${CTL}^{⋆}$ family-based model checking using variability abstractions and modal transition systems
Abstract
Variational systems can produce a (potentially huge) number of related systems, known as products or variants, by using features (configuration options) to mark the variable functionality. In many of the application domains, their rigorous ... $^{}$ $^{}$
Family-Based Model Checking with mCRL2
Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering - Volume 10202

Family-based model checking targets the simultaneous verification of multiple system variants, a technique to handle feature-based variability that is intrinsic to software product lines SPLs. We present an approach for family-based verification based ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

SPLC '17: Proceedings of the 21st International Systems and Software Product Line Conference - Volume B

September 2017

158 pages

ISBN:9781450351195

DOI:10.1145/3109729

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

Fidetia

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 September 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Short-paper
Research
Refereed limited

Conference

SPLC '17

SPLC '17: 21st International Systems and Software Product Line Conference

September 25 - 29, 2017

Sevilla, Spain

Acceptance Rates

Overall Acceptance Rate 167 of 463 submissions, 36%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
50
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kishi T(2023)Family-based Model Checking using Probabilistic Model Checker PRISM2023 30th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC60848.2023.00048(376-385)Online publication date: 4-Dec-2023
https://doi.org/10.1109/APSEC60848.2023.00048
Bunte OGroote JKeiren JLaveaux MNeele Tde Vink EWesselink WWijs AWillemse T(2019)The mCRL2 Toolset for Analysing Concurrent SystemsAdvances in Knowledge Discovery and Data Mining10.1007/978-3-030-17465-1_2(21-39)Online publication date: 3-Apr-2019
https://doi.org/10.1007/978-3-030-17465-1_2

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents