, 44:18 | Cite as

Design variability verification in Software Product Lines

  • Ganesh Khandu NarwaneEmail author
  • Jean-Vivien Millo
  • Shankara Narayanan Krishna
  • S Ramesh


This paper proposes a novel notion called variability verification applicable to Software Product Lines (SPL). Variability is central to SPL and we have observed that variability is expressed differently at different levels of abstraction in the development flow of SPL. A natural problem in this context is the conformance of variability information expressed at different levels. Design variability verification, in particular, checks whether the variability expressed at the design level conforms to that at the requirement level. Unlike many existing approaches to SPL modelling, our work does not assume a single global view of variation points, even within the same level of abstraction. In our view, an SPL is a concurrent composition of features, where each feature exhibits independent variability. This enables incremental addition of variability. The procedure is compositional in the sense that the verification of an entire SPL consisting of multiple features is reduced to the verification of the individual features. Feature level verification essentially involves standard model checking while, in the second step, a Quantified Boolean Formula (QBF) is synthesized and solved. The method has been implemented and demonstrated in a tool SPL Engine for Design Verification (SPLEnD) on a couple of fairly large case studies. SPLEnD uses SPIN tool for the feature level conformance, while the state-of-the-art QBF solver CirQit is used for the SPL level conformance. SPLEnD easily handles the evolution of SPL by addition of new features and modification of existing features. Experimental results with SPLEnD look very promising.


Software Product Lines variability verification SPIN QBF 


  1. 1.
    Kang K C, Cohen S G, Hess J A, Novak W E and Spencer Peterson A 1990 Feature-oriented domain analysis (FODA) feasibility study. Technical Report CMU/SEI-90-TR-21, Software Engineering Institute of Carnegie Mellon University, NovemberGoogle Scholar
  2. 2.
    Czarnecki K and Eisenecker U W 2000 Generative programming–methods, tools and applications. Addison-WesleyGoogle Scholar
  3. 3.
    Metzger A and Pohl K 2007 Variability management in software product line engineering. In ICSE Companion, pp. 186–187Google Scholar
  4. 4.
    Tischer C, Boss B, Müller A, Thums A, Acharya R and Schmid K 2012 Developing long-term stable product line architectures. In: Proceedings of the 16th International Software Product LineConference—SPLC ’12, vol. 1, pp. 86–95. ACM, New York, NY, USAGoogle Scholar
  5. 5.
    Cordy M, Schobbens P Y, Heymans P and Legay A 2013 Beyond boolean product-line model checking: dealing with feature attributes and multi-features. In David Notkin, Betty H. C. Cheng, and Klaus Pohl, editors, ICSE, pp. 472–481. IEEE/ACMGoogle Scholar
  6. 6.
    Classen A, Heymans P, Schobbens P Y and Legay A 2011 Symbolic model checking of software product lines. In: Proceedings of ICSE 2011, pp. 321–330Google Scholar
  7. 7.
    ter Beek M H, Gnesi S and Mazzanti F 2013 VMC: a tool for the analysis of variability in software product lines. ERCIM News, 2013(93)Google Scholar
  8. 8.
    Holzmann G J 2003 The SPIN model checker: primer and reference manual. Addison-Wesley ProfessionalGoogle Scholar
  9. 9.
    Goultiaeva A and Bacchus F 2010 Exploiting QBF duality on a circuit representation. In: Proceedings of AAAI Google Scholar
  10. 10.
    Milner R 1982 A calculus of communicating systems. Springer, New York, Inc., Secaucus, NJ, USAzbMATHGoogle Scholar
  11. 11.
    Hoare C A R 1978 Communicating sequential processes. Commun. ACM 21(8): 666–677CrossRefGoogle Scholar
  12. 12.
    Vardi M Y and Wolper P 1986 An automata-theoretic approach to automatic program verification. In: Proceedings of LICS 1986, pp. 322–331Google Scholar
  13. 13.
    Narwane G K, Millo J V, Ramesh S and Krishna S N 2016 SPLEnD website.
  14. 14.
  15. 15.
    Goultiaeva A and Bacchus F 2010 CirQit website.,
  16. 16.
    Huth M and Ryan M 2004 Logic in computer science: modelling and reasoning about systems. Cambridge University Press, New York, NY, USACrossRefGoogle Scholar
  17. 17.
    Computer Systems Group/Generative Software Development Lab 2013 Softwareproduct lines online tools. University of Waterloo, Canada, October 2013Google Scholar
  18. 18.
    Apel S, Speidel H, Wendler P, Rhein A and Beyer D 2011 Detection of feature interactions using feature-aware verification. In: Proceedings of ASE, pp. 372–375Google Scholar
  19. 19.
    Apel S and Hutchins D 2010 A calculus for uniform feature composition. ACM Trans. Program. Lang. Syst. 32(5)CrossRefGoogle Scholar
  20. 20.
    Li H C, Krishnamurthi S and Fisler K 2002 Verifying cross-cuttingfeatures as open systems. In: Proceedings of FSE, pp. 89–98Google Scholar
  21. 21.
    Fischbein D, Uchitel S and Braberman V 2006 A foundation forbehavioural conformance in software product line architectures. In: Proceedings of ROSATEA, pp. 39–48Google Scholar
  22. 22.
    Cordy M, Classen A, Perrouin G, Schobbens P Y, Heymans P and Legay A 2012 Simulation-based abstractions for software product-line model checking. In: Proceedings of ICSE, pp. 672–682Google Scholar
  23. 23.
    Asirelli P, terBeek M H, Gnesi S and Fantechi A 2011 Formal description of variability in product line families. In: Proceedings of SPLC, pp. 130–139Google Scholar
  24. 24.
    Schaefer I, Gurov D and Soleimanifard S 2010 Compositional algorithmic verification of software product lines. In: Proceedings of FMCO, pp. 184–203Google Scholar
  25. 25.
    Gondal A, Poppleton M and Butler M 2011 Composing event-B specifications---case study experience. In: Software Composition, pp. 100–115Google Scholar
  26. 26.
    Mannion M 2002 Using first-order logic for product line model validation. In: Proceedings of SPLC, pp. 176–187Google Scholar
  27. 27.
    Batory D S 2005 Feature models, grammars, and propositional formulas. In: J Henk Obbink and Klaus Pohl, editors, Proceedings of SPLC, volume 3714 of Lecture Notes in Computer Science, pp. 7–20. SpringerGoogle Scholar
  28. 28.
    Larsen K G, Nyman U and Wasowski A 2007 Modal i/o automata for interface and product line theories. In: Proceedings of the 16th European Conference on Programming, ESOP’07, pp. 64–79. Springer, Berlin, HeidelbergGoogle Scholar
  29. 29.
    Raclet J B, Badouel E, Benveniste A, Caillaud B, Legay A and Passerone R 2009 Modal interfaces: unifying interface automata and modal specifications. In: Proceedings of EMSOFT, pp. 87–96Google Scholar
  30. 30.
    Fantechi A and Gnesi S 2008 Formal modeling for product families engineering. In: SPLC’08, editor, Proceedings of SPLC’08, pp. 193–202. IEEE Computer SocietyGoogle Scholar
  31. 31.
    Gruler A, Leucker M and Scheidemann K D 2008 Calculating and modeling common parts of software product lines. In: Proceedings of SPLC, pp. 203–212Google Scholar
  32. 32.
    Gomaa H and Olimpiew E M 2008 Managing variability in reusable requirement models for software product lines. In: Proceedings of ICSR, pp. 182–185Google Scholar
  33. 33.
    Jörges S, Lamprecht A L, Margaria T, Schaefer I and Steffen B 2012 A constraint-based variability modeling framework. Int. J. Softw. Tools Technol. Transf. 14(5): 511–530CrossRefGoogle Scholar
  34. 34.
    Berg K, Bishop J and Muthig D 2005 Tracing software product linevariability: from problem to solution space. In: Proceedings of the 2005 Annual Research Conference of the South African Instituteof Computer Scientists and Information Technologists on IT Researchin Developing Countries, SAICSIT ’05, pp. 182–191. South African Institute for Computer Scientists andInformation Technologists, Republic of South AfricaGoogle Scholar
  35. 35.
    Metzger A, Heymans P, Pohl K, Schobbens P Y and Saval G 2007 Disambiguating the documentation of variability in software product lines: a separation of concerns, formalization and automated analysis. In: Proceedings of the RE Conference, pp. 243–253Google Scholar
  36. 36.
    Riebisch M and Brcina R 2008 Optimizing design for variability using traceability links. In: Proceedings of the ECBS Conference, pp. 235–244Google Scholar
  37. 37.
    terBeek M H, Mazzanti F and Sulova A 2012 VMC: a tool for product variability analysis. In: Proceedings of the FM Symposium, pp. 450–454Google Scholar
  38. 38.
    terBeek M H, Gnesi S and Mazzanti F 2012 Demonstration of a model checker for the analysis of product variability. In: Proceedings of SPLC, pp. 242–245Google Scholar
  39. 39.
    Krishnamurthi S and Fisler K 2007 Foundations of incremental aspect model-checking. ACM Trans. Softw. Eng. Methodol. 16(2)CrossRefGoogle Scholar
  40. 40.
    Liu J, Basu S and Lutz R R 2011 Compositional model checking of software product lines using variation point obligations. Autom. Softw. Eng. 18(1): 39–76CrossRefGoogle Scholar
  41. 41.
    Cordy M, Schobbens P Y, Heymans P and Legay A 2012 Behavioural modelling and verification of real-time software product lines. In: Proceedings of SPLC, pp. 66–75Google Scholar
  42. 42.
    Lauenroth K, Metzger A and Pohl K 2011 Quality assurance in the presence of variability. Technical report, SSE, Institut fur Informatik und Wirtschaftsinformatik, univertitat Duisburg EssenGoogle Scholar
  43. 43.
    Gruler A, Leucker M and Scheidemann K 2008 Modeling and model checking software product lines. In: Proceedings of the 10th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS ’08, pp. 113–131. Springer, Berlin, HeidelbergGoogle Scholar

Copyright information

© Indian Academy of Sciences 2019

Authors and Affiliations

  • Ganesh Khandu Narwane
    • 1
    Email author
  • Jean-Vivien Millo
    • 2
  • Shankara Narayanan Krishna
    • 3
  • S Ramesh
    • 2
  1. 1.Homi Bhabha National InstituteMumbaiIndia
  2. 2.Global General Motors R&DTCI BangaloreBangaloreIndia
  3. 3.Department of Computer Science and EngineeringIndian Institute of Technology BombayMumbaiIndia

Personalised recommendations