Andreas Classen
Pierre-Yves Schobbens
ABSTRACT
In product line engineering, systems are developed in families and differences between family members are expressed in terms of features. Formal modelling and verification is an important issue in this context as more and more critical systems are developed this way. Since the number of systems in a family can be exponential in the number of features, two major challenges are the scalable modelling and the efficient verification of system behaviour. Currently, the few attempts to address them fail to recognise the importance of features as a unit of difference, or do not offer means for automated verification.
In this paper, we tackle those challenges at a fundamental level. We first extend transition systems with features in order to describe the combined behaviour of an entire system family. We then define and implement a model checking technique that allows to verify such transition systems against temporal properties. An empirical evaluation shows substantial gains over classical approaches.
- D. Alrajeh, J. Kramer, A. Russo, and S. Uchitel. Learning operational requirements from goal models. In ICSE 31, pages 265--275, 2009. Google Scholar
Digital Library
- P. Asirelli, M. H. ter Beek, S. Gnesi, and A. Fantechi. Deontic logics for modeling behavioural variability. In VaMoS'09, pages 71--76, 2009.Google Scholar
- F. Bachmann, M. Goedicke, J. C. S. do Prado Leite, R. L. Nord, K. Pohl, B. Ramesh, and A. Vilbig. A meta-model for representing variability in product family development. In Int. Workshop on Product Family Engineering (PPE), pages 66--80, 2003.Google Scholar
- C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2007.Google Scholar
- 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. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999. Google ScholarDigital Library
- A. Classen. Modelling with FTS: a collection of illustrative examples. Technical Report P-CS-TR SPLMC-00000001, PReCISE Research Center, University of Namur, Namur, Belgium, 2010. www.info.fundp.ac.be/~acs/fts.Google Scholar
- A. Classen, P. Heymans, and P.-Y. Schobbens. What's in a feature: A requirements engineering perspective. In FASE'08, Held as Part of ETAPS'08, volume 4961 of LNCS, pages 16--30. Springer, 2008. 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. SEI Series in Software Engineering. Addison-Wesley, August 2001.Google ScholarDigital Library
- C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory-efficient algorithms for the verification of temporal properties. Form. Methods Syst. Des., 1(2--3):275--288, 1992. 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
- K. Czarnecki and K. Pietroszek. Verifying feature-based model templates against well-formedness OCL constraints. In GPCE '06, pages 211--220. ACM, 2006. Google ScholarDigital Library
- C. Ebert and C. Jones. Embedded software: Facts, figures, and future. Computer, 42(4):42--52, 2009. Google ScholarDigital Library
- E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS 32, pages 368--377. IEEE, 1991. Google ScholarDigital Library
- A. Fantechi and S. Gnesi. A behavioural model for product families. In ESEC-FSE'07, Companion, 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
- P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In CAV 2001, number 2102 in LNCS, pages 53--65, 2001. 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 CMU/SEI-90-TR-21, SEI, CMU, November 1990.Google ScholarCross Ref
- J. Kramer, J. Magee, M. Sloman, and A. Lister. Conic: an integrated approach to distributed computer control systems. Computers and Digital Techniques, IEE Proceedings E, 130(1):1--10, 1983.Google ScholarCross Ref
- 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, 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
- M. Mendonca, A. Wasowski, and K. Czarnecki. SAT-based analysis of feature models is easy. In SPLC'09, pages 231--240, 2009. Google ScholarDigital Library
- B. Morin, O. Barais, G. Nain, and J.-M. Jézéquel. Taming dynamically adaptive systems using models and aspects. In ICSE '09, pages 122--132. IEEE, 2009. Google ScholarDigital Library
- M. Plath and M. Ryan. Feature integration using a feature construct. Sci. Comput. Program., 41(1):53--84, 2001. Google ScholarDigital Library
- P. Schnoebelen. The complexity of temporal logic model checking. In Advances in Modal Logic 4, pages 393--436, 2002.Google Scholar
- 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
- W. M. P. van der Aalst, M. Dumas, F. Gottschalk, A. H. M. ter Hofstede, M. L. Rosa, and J. Mendling. Correctness-preserving configuration of business process models. In FASE'08, Held as Part of ETAPS'08, pages 46--61, 2008. Google ScholarDigital Library
- M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS'86, pages 332--344. IEEE CS, 1986.Google Scholar
- 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
Recommendations
Symbolic model checking of software product lines
ICSE '11: Proceedings of the 33rd International Conference on Software EngineeringWe 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 ...
A Classification and Survey of Analysis Strategies for Software Product Lines
Software-product-line engineering has gained considerable momentum in recent years, both in industry and in academia. A software product line is a family of software products that share a common set of features. Software product lines challenge ...
Static Analysis of Featured Transition Systems
SPLC '19: Proceedings of the 23rd International Systems and Software Product Line Conference - Volume AA Featured Transition System (FTS) is a formal behavioural model for software product lines, which represents the behaviour of all the products of an SPL in a single compact structure by associating transitions with features that condition their ...
Comments