Synthesis-Based Variability Control: Correctness by Construction

  • Anna-Lena Lamprecht
  • Tiziana Margaria
  • Ina Schaefer
  • Bernhard Steffen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7542)


In this paper, we show the power of combining modern synthesis technology with a constraint-oriented approach to variability modeling. This combination guarantees the validity of all the required properties simply by construction: including a new property simply requires adding a corresponding constraint. The synthesis procedure will then automatically take care that all generated variants are property-conform. This fully declarative approach leads to a very agile variability modeling framework, where new product lines guaranteeing new properties can be defined ad hoc and are, due to our synthesis technology, immediately operational. As the underlying constraint language allows fully describing the intended solution space without imposing any overspecification, neither on the structure, nor on the artifacts, our approach may in particular be regarded as a step from the today typical settings with closed-world assumption to one with an open-world assumption. Impact and ease of this method are illustrated along a small case study running on our prototypical framework implementation.


Model Check Temporal Logic Software Product Line Label Transition System Variability Modeling 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Pohl, K., Böckle, G., van der Linden, F.: Software Product Line Engineering - Foundations, Principles, and Techniques. Springer (2005)Google Scholar
  2. 2.
    Sinnema, M., Deelstra, S.: Classifying variability modeling techniques. Information and Software Technology 49(7), 717–739 (2006)CrossRefGoogle Scholar
  3. 3.
    Czarnecki, K.: Variability Modeling: State of the Art and Future Directions. In: VaMoS, ICB-Research Report No. 37, University of Duisburg Essen, p. 11 (2010)Google Scholar
  4. 4.
    Chen, L., Babar, M.A.: A systematic review of evaluation of variability management approaches in software product lines. Information and Software Technology 53(4), 344–362 (2011)CrossRefGoogle Scholar
  5. 5.
    Thüm, T., Schaefer, I., Kuhlemann, M., Apel, S.: Proof composition for deductive verification of software product lines. In: Proc. Int’l Workshop Variability-intensive Systems Testing, Validation and Verification (VAST), pp. 270–277. IEEE Computer Society (2011)Google Scholar
  6. 6.
    Lochau, M., Oster, S., Goltz, U., Schürr, A.: Model-based Pairwise Testing for Feature Interaction Coverage in Software Product Line Engineering. Software Quality Journal, 1–38 (2011)Google Scholar
  7. 7.
    Bruns, D., Klebanov, V., Schaefer, I.: Verification of Software Product Lines with Delta-Oriented Slicing. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 61–75. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  8. 8.
    Schaefer, I., Rabiser, R., Clarke, D., Bettini, L., Benavides, D., Botterweck, G., Pathak, A., Trujilol, S., Villela, K.: Software Diversity – State of the Art and Perspectives. STTT (2012)Google Scholar
  9. 9.
    Classen, A., Heymans, P., Schobbens, P.Y., Legay, A., Raskin, J.F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering (ICSE 2010), vol. 1, pp. 335–344. ACM, New York (2010)CrossRefGoogle Scholar
  10. 10.
    Asirelli, P., ter Beek, M.H., Gnesi, S., Fantechi, A.: Deontic logics for modeling behavioural variability. In: VaMoS, Essen, Germany, pp. 71–76 (January 2009)Google Scholar
  11. 11.
    Apel, S., Kästner, C., Grösslinger, A., Lengauer, C.: Type safety for feature-oriented product lines. Automated Software Engineering 17(3), 251–300 (2010)CrossRefGoogle Scholar
  12. 12.
    Kästner, C., Apel, S., Thüm, T., Saake, G.: Type checking annotation-based product lines. ACM Transactions on Software Engineering and Methodology (TOSEM) (to appear, 2012)Google Scholar
  13. 13.
    Cordy, M., Classen, A., Perrouin, G., Heymans, P., Schobbens, P.Y., Legay, A.: Simulation Relation for Software Product Lines: Foundations for Scalable Model Checking. In: Proceedings of 34th International Conference on Software Engineering (ICSE 2012). IEEE (to appear, 2012)Google Scholar
  14. 14.
    Hähnle, R., Schaefer, I.: A Liskov Principle for Delta-Oriented Programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 32–46. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  15. 15.
    Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems (TOPLAS) 16(6), 1811–1841 (1994)CrossRefGoogle Scholar
  16. 16.
    Delaware, B., Cook, W., Batory, D.: A Machine-Checked Model of Safe Composition. In: 8th Workshop on Foundations of Aspect-Oriented Languages (FOAL 2009), pp. 31–35. ACM (2009)Google Scholar
  17. 17.
    Schaefer, I., Bettini, L., Damiani, F.: Compositional type-checking for delta-oriented programming. In: 10th International Conference on Aspect-Oriented Software Development (AOSD 2011), pp. 43–56. ACM (2011)Google Scholar
  18. 18.
    Schaefer, I., Lamprecht, A.L., Margaria, T.: Constraint-oriented Variability Modeling. In: Rash, J., Rouff, C. (eds.) 34th Annual IEEE Software Engineering Workshop (SEW-34), pp. 77–83. IEEE CS Press (June 2011)Google Scholar
  19. 19.
    Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Symbolic model checking of software product lines. In: Proceedings of the 33rd International Conference on Software Engineering (ICSE 2011), pp. 321–330. ACM, New York (2011)Google Scholar
  20. 20.
    Steffen, B., Margaria, T., Freitag, B.: Module Configuration by Minimal Model Construction. Technical report, Fakultät für Mathematik und Informatik, Universität Passau (1993)Google Scholar
  21. 21.
    Freitag, B., Steffen, B., Margaria, T., Zukowski, U.: An Approach to Intelligent Software Library Management. In: Proceedings of the 4th International Conference on Database Systems for Advanced Applications (DASFAA), pp. 71–78. World Scientific Press (1995)Google Scholar
  22. 22.
    Steffen, B., Margaria, T., Braun, V.: The Electronic Tool Integration platform: concepts and design. International Journal on Software Tools for Technology Transfer (STTT) 1(1-2), 9–30 (1997)CrossRefzbMATHGoogle Scholar
  23. 23.
    Steffen, B., Margaria, T., von der Beeck, M.: Automatic synthesis of linear process models from temporal constraints: An incremental approach. In: ACM/SIGPLAN Int. Workshop on Automated Analysis of Software (AAS 1997) (1997)Google Scholar
  24. 24.
    Steffen, B., Margaria, T., Claßen, A., Braun, V., Reitenspieß, M.: An Environment for the Creation of Intelligent Network Services. In: Intelligent Networks: IN/AIN Technologies, Operations, Services and Applications - A Comprehensive Report, IEC: International Engineering Consortium, pp. 287–300 (1996)Google Scholar
  25. 25.
    Steffen, B.: Method for incremental synthesis of a discrete technical system (1998)Google Scholar
  26. 26.
    Naujokat, S., Lamprecht, A.L., Steffen, B.: Tailoring Process Synthesis to Domain Characteristics. In: Proceedings of the 16th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS) (2011)Google Scholar
  27. 27.
    Lamprecht, A.L., Margaria, T., Steffen, B.: Bio-jETI: a framework for semantics-based service composition. BMC Bioinformatics 10(suppl. 10), S8 (2009)Google Scholar
  28. 28.
    Lamprecht, A.L., Naujokat, S., Margaria, T., Steffen, B.: Semantics-based composition of EMBOSS services. Journal of Biomedical Semantics 2(suppl. 1), S5 (2011)Google Scholar
  29. 29.
    Lamprecht, A.L., Naujokat, S., Steffen, B., Margaria, T.: Constraint-Guided Workflow Composition Based on the EDAM Ontology. In: Burger, A., Marshall, M.S., Romano, P., Paschke, A., Splendiani, A. (eds.) Proceedings of the 3rd Workshop on Semantic Web Applications and Tools for Life Sciences (SWAT4LS 2010). CEUR Workshop Proceedings, vol. 698 (December 2010)Google Scholar
  30. 30.
    Lamprecht, A.L., Naujokat, S., Margaria, T., Steffen, B.: Synthesis-Based Loose Programming. In: Proceedings of the 7th International Conference on the Quality of Information and Communications Technology (QUATIC) (September 2010)Google Scholar
  31. 31.
    Naujokat, S., Lamprecht, A.-L., Steffen, B.: Loose Programming with PROPHETS. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 94–98. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  32. 32.
    Lamprecht, A.L., Margaria, T., Steffen, B., Sczyrba, A., Hartmeier, S., Giegerich, R.: GeneFisher-P: variations of GeneFisher as processes in Bio-jETI. BMC Bioinformatics 9(suppl. 4), S13 (2008)Google Scholar
  33. 33.
    Ebert, B.E.: A systems approach to understand and engineer whole-cell redox biocatalysts. Dissertation, Fakultät Bio- und Chemieingenieurwesen, Technische Universität Dortmund (2011)Google Scholar
  34. 34.
    Steffen, B., Margaria, T., Claßen, A., Braun, V., Nisius, R., Reitenspieß, M.: A Constraint-Oriented Service Creation Environment. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 418–421. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  35. 35.
    Steffen, B., Margaria, T.: MetaFrame in Practice: Design of Intelligent Network Services. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 390–415. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  36. 36.
    Margaria, T., Steffen, B.: Aggressive Model-Driven Development: Synthesizing Systems from Models viewed as Constraints. In: MBEES, pp. 51–62 (2005)Google Scholar
  37. 37.
    Margaria, T., Steffen, B.: Agile IT: Thinking in User-Centric Models. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 490–502. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  38. 38.
    Jörges, S., Lamprecht, A.L., Margaria, T., Schaefer, I., Steffen, B.: A Constraint-based Variability Modeling Framework. International Journal on Software Tools for Technology Transfer (STTT) (to appear, 2012)Google Scholar
  39. 39.
    Margaria, T., Steffen, B.: Business Process Modelling in the jABC: The One-Thing-Approach. In: Cardoso, J., van der Aalst, W. (eds.) Handbook of Research on Business Process Modeling. IGI Global (2009)Google Scholar
  40. 40.
    Steffen, B.: Unifying Models. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 1–20. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  41. 41.
    Steffen, B., Rüthing, O.: Quality Engineering: Leveraging Heterogeneous Information (Invited Talk). In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 23–37. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  42. 42.
    Margaria, T., Steffen, B.: Service-Orientation: Conquering Complexity with XMDD. In: Hinchey, M., Coyle, L. (eds.) Conquering Complexity, pp. 217–236. Springer, London (2012)CrossRefGoogle Scholar
  43. 43.
    Steffen, B., Margaria, T., Claßen, A., Braun, V.: Incremental Formalization: A Key to Industrial Success. Software - Concepts and Tools 17(2), 78–95 (1996)Google Scholar
  44. 44.
    Steffen, B., Margaria, T., Nagel, R., Jörges, S., Kubczak, C.: Model-Driven Development with the jABC. In: Bin, E., Ziv, A., Ur, S. (eds.) HVC 2006. LNCS, vol. 4383, pp. 92–108. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  45. 45.
    Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The description logic handbook: theory, implementation, and applications. Cambridge University Press, New York (2003)zbMATHGoogle Scholar
  46. 46.
    Schreiber, G., Dean, M.: OWL Web Ontology Language Reference. W3C Recommendation (2004), (last accessed June 25, 2012)
  47. 47.
    May, C.: Entwicklung einer Bibliothek zur service-orientierten Modellierung von Ontologien. Diploma thesis, TU Dortmund (2009)Google Scholar
  48. 48.
    Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A Logical Framework to Deal with Variability. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 43–58. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  49. 49.
    Asirelli, P., ter Beek, M.H., Gnesi, S., Fantechi, A.: Formal Description of Variability in Product Families. In: 15th International Software Product Line Conference, SPLC 2011, pp. 130–139 (2011)Google Scholar
  50. 50.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Temporal Logics. In: Model Checking, pp. 27–32. The MIT Press (1999)Google Scholar
  51. 51.
    Apel, S., Kästner, C.: An Overview of Feature-Oriented Software Development. Journal of Object Technology 8(5), 49–84 (2009)CrossRefGoogle Scholar
  52. 52.
    Larsen, K., Thomsen, B.: A modal process logic. In: Proceedings of the Third Annual Symposium on Logic in Computer Science, LICS 1988, pp. 203–210 (July 1988)Google Scholar
  53. 53.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32, 137–161 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  54. 54.
    Steffen, B.: Property-Oriented Expansion. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 22–41. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  55. 55.
    Steffen, B.: Characteristic Formulae. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 723–732. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  56. 56.
    Steffen, B., Ingólfsdóttir, A.: Characteristic Formulae for Processes with Divergence. Information and Computation 110(1), 149–163 (1994)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Anna-Lena Lamprecht
    • 1
  • Tiziana Margaria
    • 1
  • Ina Schaefer
    • 2
  • Bernhard Steffen
    • 3
  1. 1.Chair for Service and Software EngineeringUniversity of PotsdamGermany
  2. 2.Institut für Softwaretechnik und FahrzeuginformatikTechnische Universität BraunschweigGermany
  3. 3.Chair for Programming SystemsTechnical University DortmundGermany

Personalised recommendations