Andreas Classen
Pierre-Yves Schobbens
ABSTRACT
We study the problem of model checking software product line (SPL) behaviours against temporal properties. This is more difficult than for single systems because an SPL with n features yields up to 2n individual systems to verify. As each individual verification suffers from state explosion, it is crucial to propose efficient formalisms and heuristics.
We recently proposed featured transition systems (FTS), a compact representation for SPL behaviour, and defined algorithms for model checking FTS against linear temporal properties. Although they showed to outperform individual system verifications, they still face a state explosion problem as they enumerate and visit system states one by one.
In this paper, we tackle this latter problem by using symbolic representations of the state space. This lead us to consider computation tree logic (CTL) which is supported by the industry-strength symbolic model checker NuSMV. We first lay the foundations for symbolic SPL model checking by defining a feature-oriented version of CTL and its dedicated algorithms. We then describe an implementation that adapts the NuSMV language and tool infrastructure. Finally, we propose theoretical and empirical evaluations of our results. The benchmarks show that for certain properties, our algorithm is over a hundred times faster than model checking each system with the standard algorithm.
- http://www.info.fundp.ac.be/~acs/fts, 2010.Google Scholar
- P. Asirelli, M. H. ter Beek, A. Fantechi, and S. Gnesi. A logical framework to deal with variability. In 8th IFM, number 6396 in LNCS, pages 43--58. Springer, 2010. Google ScholarDigital Library
- P. Asirelli, M. H. ter Beek, S. Gnesi, and A. Fantechi. A deontic logical framework for modelling product families. In VaMoS'10, pages 37--44, 2010.Google Scholar
- C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2007.Google Scholar
- D. Batory, D. Benavides, and A. Ruiz-Cortes. Automated analysis of feature models: Challenges ahead. Comm. ACM, 49(12):45--47, 2006. Google ScholarDigital Library
- R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv., 24(3):293--318, 1992. Google ScholarDigital Library
- J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Inf. Comp., 98(2):142--170, 1992. Google ScholarDigital Library
- M. Calder, M. Kolberg, E. H. Magill, and S. Reiff-Marganiec. Feature interaction: a critical review and considered forecast. Computer Networks, 41(1):115--141, 2003. Google ScholarDigital Library
- E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, volume 131 of LNCS, pages 52--71. Springer, 1981. Google ScholarDigital Library
- A. Classen. CTL model checking for software product lines in NuSMV. Technical Report P-CS-TR SPLMC-00000002, University of Namur, 2010.Google Scholar
- A. Classen. Modelling with FTS: a collection of illustrative examples. Technical Report P-CS-TR SPLMC-00000001, University of Namur, 2010.Google Scholar
- A. Classen, P. Heymans, and P.-Y. Schobbens. What's in a feature: A requirements engineering perspective. In FASE'08, volume 4961 of LNCS, pages 16--30, 2008. 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 32, pages 335--344. IEEE, 2010. Google ScholarDigital Library
- A. Classen, P. Heymans, T. T. Tun, and B. Nuseibeh. Towards safer composition. In ICSE 31, Companion Volume, pages 227--230. IEEE, 2009.Google ScholarCross Ref
- P. C. Clements and L. Northrop. Software Product Lines: Practices and Patterns. Addison-Wesley, 2001. Google ScholarDigital Library
- K. Czarnecki and M. Antkiewicz. Mapping features to models: A template approach based on superimposed variants. In GPCE'05, pages 422--437, 2005. Google ScholarDigital Library
- C. Ebert and C. Jones. Embedded software: Facts, figures, and future. Computer, 42(4):42--52, 2009. Google ScholarDigital Library
- A. Fantechi and S. Gnesi. A behavioural model for product families. In ESEC-FSE'07, pages 521--524. ACM, 2007. Google ScholarDigital Library
- A. Fantechi and S. Gnesi. Formal modeling for product families engineering. In SPLC 2008, pages 193--202. IEEE CS, 2008. Google ScholarDigital Library
- D. Fischbein, S. Uchitel, and V. Braberman. A foundation for behavioural conformance in software product line architectures. In ROSATEA'06, ISSTA 2006 workshop, pages 39--48. ACM Press, 2006. Google ScholarDigital Library
- N. Francez and I. Forman. Superimposition for inter- acting processes. In Concur'90, pages 230--245, 1990. Google ScholarDigital Library
- A. Gruler, M. Leucker, and K. Scheidemann. Modeling and model checking software product lines. In IFIP WG 6.1 FMOODS '08, pages 113--131. Springer, 2008. Google ScholarDigital Library
- K. Kang, S. Cohen, J. Hess, W. Novak, and S. Peterson. Feature-oriented domain analysis (FODA) feasibility study. Technical Report Carnegie Mellon University/SEI-90-TR-21, SEI, Carnegie Mellon University, November 1990.Google ScholarCross Ref
- K. G. Larsen. Modal specifications. In Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 232--246. Springer, 1989. Google ScholarDigital Library
- K. G. Larsen, U. Nyman, and A. Wasowski. Modal I/O automata for interface and product line theories. In ESOP, pages 64--79, 2007. Google ScholarDigital Library
- K. Lauenroth, S. Töhning, and K. Pohl. Model checking of domain artifacts in product line engineering. In IEEE/ACM ASE, pages 269--280, 2009. Google ScholarDigital Library
- H. C. Li, S. Krishnamurthi, and K. Fisler. Verifying cross-cutting features as open systems. In SIGSOFT FSE, pages 89--98, 2002. Google ScholarDigital Library
- J. Liu, J. Dehlinger, and R. Lutz. Safety analysis of software product lines using state-based modeling. J. Syst. Softw., 80(11):1879--1892, 2007. Google ScholarDigital Library
- K. McMillan. Symbolic Model Checking. Kluwer, 1993. Google ScholarCross Ref
- B. Morin, O. Barais, G. Nain, and J.-M. Jézéquel. Taming dynamically adaptive systems using models and aspects. In ICSE 31, pages 122--132. IEEE, 2009. Google ScholarDigital Library
- C. H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.Google Scholar
- M. Plath and M. Ryan. Feature integration using a feature construct. Sci. Comput. Program., 41(1):53--84, 2001. Google ScholarDigital Library
- A. Pnueli. The temporal logic of programs. In Proc. 18th FOCS, pages 46--57, 1977. Google ScholarDigital Library
- H. Post and C. Sinz. Configuration lifting: Verification meets software configuration. In ASE'08, pages 188--197. IEEE, 2008. Google ScholarDigital Library
- P.-Y. Schobbens, P. Heymans, J.-C. Trigaux, and Y. Bontemps. Feature Diagrams: A Survey and A Formal Semantics. In RE'06, pages 139--148, 2006. Google ScholarDigital Library
- T. T. Tun, Q. Boucher, A. Classen, A. Hubaux, and P. Heymans. Relating requirements and feature configurations: A systematic approach. In SPLC'09, pages 201--210. SEI, Carnegie Mellon University, 2009. Google ScholarDigital Library
- T. Ziadi, L. Hélouët, and J.-M. Jézéquel. Towards a UML profile for software product lines. In Int. Workshop on Product Family Engineering (PPE), pages 129--139, 2003.Google Scholar
Index Terms
- Symbolic model checking of 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 ...
Potential synergies of theorem proving and model checking for software product lines
SPLC '14: Proceedings of the 18th International Software Product Line Conference - Volume 1The verification of software product lines is an active research area. A challenge is to efficiently verify similar products without the need to generate and verify them individually. As solution, researchers suggest family-based verification approaches,...
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 ...
Comments