research-article

ProVeLines: a product line of verifiers for software product lines

Authors:

Andreas Classen,

Patrick Heymans,

Pierre-Yves Schobbens,

Axel LegayAuthors Info & Claims

SPLC '13 Workshops: Proceedings of the 17th International Software Product Line Conference co-located workshops

Pages 141 - 146

https://doi.org/10.1145/2499777.2499781

Published: 26 August 2013 Publication History

Abstract

Software Product Lines (SPLs) are families of similar software products built from a common set of features. As the number of products of an SPL is potentially exponential in the number of its features, the model checking problem is harder than for single software. A practical way to face this exponential blow-up is to reuse common behaviour between products. We previously introduced Featured Transition Systems (FTS), a mathematical model that serves as a basis for efficient SPL model checking techniques. In this paper, we present ProVeLines, a product line of verifiers for SPLs that incorporates the results of over three years of research on formal verification of SPLs. Being itself a product line, our tool is flexible and extensible, and offers a wide range of solutions for SPL modelling and verification.

References

[1]

S. Apel, H. Speidel, P. Wendler, A. von Rhein, and D. Beyer. Feature-interaction detection using feature-aware verification. In ASE'11, pages 372--375. IEEE, 2011.

Digital Library

[2]

P. Asirelli, M. H. ter Beek, A. Fantechi, and S. Gnesi. Formal description of variability in product families. In SPLC'11, pages 130--139. Springer-Verlag, 2011.

Digital Library

[3]

C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2007.

[4]

J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL in 1995. In TACAS'96, pages 431--434. Springer-Verlag, 1996.

Digital Library

[5]

R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293--318, Sept. 1992.

Digital Library

[6]

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In CAV '02, volume 2404 of LNCS. Springer, July 2002.

Digital Library

[7]

A. Classen, Q. Boucher, and P. Heymans. A text-based approach to feature modelling: Syntax and semantics of TVL. SCP, 76:1130--1143, December 2011.

Digital Library

[8]

A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens. Model checking software product lines with SNIP. STTT, 14(5):589--612, 2012.

Digital Library

[9]

A. Classen, M. Cordy, P.-Y. Schobbens, P. Heymans, A. Legay, and J.-F. cois Raskin. Featured transition systems: Foundations for verifying variability-intensive systems and their application to LTL model checking. Transactions on Software Engineering (in press), 2013.

Digital Library

[10]

A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. Symbolic model checking of software product lines. In ICSE'11, pages 321--330. ACM, 2011.

Digital Library

[11]

A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay, and J.-F. Raskin. Model checking lots of systems: efficient verification of temporal properties in software product lines. In ICSE'10, pages 335--344. ACM, 2010.

Digital Library

[12]

M. Cordy, A. Classen, G. Perrouin, P. Heymans, P.-Y. Schobbens, and A. Legay. Simulation-based abstractions for software product-line model checking. In ICSE'12, pages 672--682. IEEE, 2012.

Digital Library

[13]

M. Cordy, P. Heymans, P.-Y. Schobbens, and A. Legay. Behavioural modelling and verification of real-time software product lines. In SPLC'12. ACM, 2012.

Digital Library

[14]

M. Cordy, P.-Y. Schobbens, P. Heymans, and A. Legay. Beyond boolean product-line model checking: Dealing with feature attributes and multi-features. In ICSE'13, pages 472--481. IEEE, 2013.

Digital Library

[15]

L. De Moura and N. Bjørner. Z3: an efficient SMT solver. In TACAS'08, pages 337--340. Springer-Verlag, 2008.

Digital Library

[16]

N. Eén and N. Sörensson. An extensible sat-solver. In SAT'03, pages 502--518. Springer, 2003.

[17]

J. Greenyer, A. M. Sharifloo, M. Cordy, and P. Heymans. Efficient consistency checking of scenario-based product line specifications. In RE '12, pages 161--170, 2012.

Digital Library

[18]

G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2004.

Digital Library

[19]

K. Kang, S. Cohen, J. Hess, W. Novak, and S. Peterson. Feature-oriented domain analysis (FODA) feasibility study. Technical Report CMU/SEI-90-TR-21, 1990.

[20]

M. Plath and M. Ryan. Feature integration using a feature construct. SCP, 41(1):53--84, 2001.

Digital Library

[21]

H. Post and C. Sinz. Configuration lifting: Verification meets software configuration. In ASE'08, pages 347--350. IEEE CS, 2008.

Digital Library

[22]

P. Shaker, J. M. Atlee, and S. Wang. A feature-oriented requirements modelling language. In RE '12, pages 151--160, 2012.

Digital Library

[23]

M. H. ter Beek, F. Mazzanti, and A. Sulova. Vmc: A tool for product variability analysis. In FM '12, pages 450--454, 2012.

Cited By

Weis KTeixeira LDubslaff CApel SFilkov VRay BZhou M(2024)Blackbox Observability of Features and Feature InteractionsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695490(1120-1132)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695490
Casaluce RBurattin AChiaromonte FLafuente AVandin A(2024)White-box validation of quantitative product lines by statistical model checking and process miningJournal of Systems and Software10.1016/j.jss.2024.111983210:COnline publication date: 1-Apr-2024
https://dl.acm.org/doi/10.1016/j.jss.2024.111983
Dimovski ALazreg SCordy MLegay A(2023)Family-based model checking of fMultiLTL propertiesProceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A10.1145/3579027.3608976(41-51)Online publication date: 28-Aug-2023
https://dl.acm.org/doi/10.1145/3579027.3608976
Show More Cited By

Index Terms

ProVeLines: a product line of verifiers for software product lines
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Behavioural modelling and verification of real-time software product lines
SPLC '12: Proceedings of the 16th International Software Product Line Conference - Volume 1

In Software Product Line (SPL) engineering, software products are build in families rather than individually. Many critical software are nowadays build as SPLs and most of them obey hard real-time requirements. Formal methods for verifying SPLs are thus ...
Managing evolution in software product lines: a model-checking perspective
VaMoS '12: Proceedings of the 6th International Workshop on Variability Modeling of Software-Intensive Systems

In Software Product Line (SPL) engineering, similar software products are developed in families rather than individually. Developing similar software at once leads to new challenges. In particular, the model checking problem for SPL is harder because it ...
Model checking software product lines with SNIP

We present SNIP, an efficient model checker for software product lines (SPLs). Variability in software product lines is generally expressed in terms of features, and the number of potential products is exponential in the number of features. Whereas ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

SPLC '13 Workshops: Proceedings of the 17th International Software Product Line Conference co-located workshops

August 2013

148 pages

ISBN:9781450323253

DOI:10.1145/2499777

Copyright © 2013 Copyright is held by the owner/author(s).

Permission to make digital or hard copies of part or all 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 third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 August 2013

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLC 2013 workshops

SPLC 2013 workshops: 17th International Software Product Line Conference co-located workshops

August 26 - 30, 2013

Tokyo, Japan

Acceptance Rates

Overall Acceptance Rate 167 of 463 submissions, 36%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

58
Total Citations
View Citations
234
Total Downloads

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

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Weis KTeixeira LDubslaff CApel SFilkov VRay BZhou M(2024)Blackbox Observability of Features and Feature InteractionsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695490(1120-1132)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695490
Casaluce RBurattin AChiaromonte FLafuente AVandin A(2024)White-box validation of quantitative product lines by statistical model checking and process miningJournal of Systems and Software10.1016/j.jss.2024.111983210:COnline publication date: 1-Apr-2024
https://dl.acm.org/doi/10.1016/j.jss.2024.111983
Dimovski ALazreg SCordy MLegay A(2023)Family-based model checking of fMultiLTL propertiesProceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A10.1145/3579027.3608976(41-51)Online publication date: 28-Aug-2023
https://dl.acm.org/doi/10.1145/3579027.3608976
Kaya DTuglular TBelli F(2023)Software Product Line Testing based on Event Sequence Graphs with Feature Expressions2023 8th International Conference on Computer Science and Engineering (UBMK)10.1109/UBMK59864.2023.10286660(175-180)Online publication date: 13-Sep-2023
https://doi.org/10.1109/UBMK59864.2023.10286660
Dubslaff CWeis KBaier CApel SDwyer MDamian DZeller A(2022)Causality in configurable software systemsProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510200(325-337)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510200
ter Beek MDamiani FLienhardt MMazzanti FPaolini LScarso G(2022)FTS4VMCScience of Computer Programming10.1016/j.scico.2022.102879224:COnline publication date: 1-Dec-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102879
Fahrenberg ULegay A(2022)Featured gamesScience of Computer Programming10.1016/j.scico.2022.102874(102874)Online publication date: Sep-2022
https://doi.org/10.1016/j.scico.2022.102874
Cazzola WFavalli L(2022)Towards a recipe for language decomposition: quality assessment of language product linesEmpirical Software Engineering10.1007/s10664-021-10074-627:4Online publication date: 1-Jul-2022
https://dl.acm.org/doi/10.1007/s10664-021-10074-6
Lazreg SCordy MLegay A(2022)Verification of Variability-Intensive Stochastic Systems with Statistical Model CheckingLeveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning10.1007/978-3-031-19759-8_27(448-471)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-19759-8_27
Beek MMazzanti FDamiani FPaolini LScarso GValfrè MLienhardt MMousavi MSchobbens P(2021)Static analysis and family-based model checking of featured transition systems with VMCProceedings of the 25th ACM International Systems and Software Product Line Conference - Volume B10.1145/3461002.3473071(24-27)Online publication date: 6-Sep-2021
https://dl.acm.org/doi/10.1145/3461002.3473071
Show More Cited By

View Options

Get Access

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