Maxime Cordy
Pierre-Yves Schobbens
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.
- 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. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2007.Google Scholar
- J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL in 1995. In TACAS'96, pages 431--434. Springer-Verlag, 1996. Google ScholarDigital Library
- R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293--318, Sept. 1992. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- L. De Moura and N. Bjørner. Z3: an efficient SMT solver. In TACAS'08, pages 337--340. Springer-Verlag, 2008. Google ScholarDigital Library
- N. Eén and N. Sörensson. An extensible sat-solver. In SAT'03, pages 502--518. Springer, 2003.Google Scholar
- 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. Google ScholarDigital Library
- G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2004. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- M. Plath and M. Ryan. Feature integration using a feature construct. SCP, 41(1):53--84, 2001. Google ScholarDigital Library
- H. Post and C. Sinz. Configuration lifting: Verification meets software configuration. In ASE'08, pages 347--350. IEEE CS, 2008. Google ScholarDigital Library
- P. Shaker, J. M. Atlee, and S. Wang. A feature-oriented requirements modelling language. In RE '12, pages 151--160, 2012. Google ScholarDigital Library
- M. H. ter Beek, F. Mazzanti, and A. Sulova. Vmc: A tool for product variability analysis. In FM '12, pages 450--454, 2012.Google Scholar
Index Terms
- ProVeLines: a product line of verifiers for software product lines
Recommendations
Behavioural modelling and verification of real-time software product lines
SPLC '12: Proceedings of the 16th International Software Product Line Conference - Volume 1In 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 SystemsIn 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