Safe composition of product lines

ABSTRACT

Programs of a software product line can be synthesized by composing modules that implement features. Besides high-level domain constraints that govern the compatibility of features, there are also low-level implementation constraints: a feature module can reference elements that are defined in other feature modules. Safe composition is the guarantee that all programs in a product line are type safe: i.e., absent of references to undefined elements (such as classes, methods, and variables). We show how safe composition properties can be verified for AHEAD product lines using feature models and SAT solvers.

REFERENCES

• 1: M. Anastasopoulos and D. Muthig. "An Evaluation of Aspect-Oriented Programming as a Product Line Implementation Technology". ICSR 2004.
• 2: D. Ancona , G. Lagorio , E. Zucca, True separate compilation of Java classes, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.189-200, October 06-08, 2002, Pittsburgh, PA, USA [doi>10.1145/571157.571177]
• 3: Apache Ant Project. http://ant.apache.org/
• 4: I. Aracic, V. Gasiunas, M. Mezini, and K. Ostermann. "An Overview of CaesarJ", Journal of Aspect Oriented Development, 2006.
• 5: Argonne National Laboratory. "Otter: An Automated Deduction System", www-unix.mcs.anl.gov/AR/otter/
• 6: Don Batory , Sean O'Malley, The design and implementation of hierarchical software systems with reusable components, ACM Transactions on Software Engineering and Methodology (TOSEM), v.1 n.4, p.355-398, Oct. 1992 [doi>10.1145/136586.136587]
• 7: D. Batory , B. Lofaso , Y. Smaragdakis, JTS: Tools for Implementing Domain-Specific Languages, Proceedings of the 5th International Conference on Software Reuse, p.143, June 02-05, 1998
• 8: Don Batory , Rich Cardone , Yannis Smaragdakis, Object-oriented framework and product lines, Proceedings of the first conference on Software product lines : experience and research directions: experience and research directions, p.227-247, November 2000, Denver, Colorado, United States
• 9: D. Batory, AHEAD Tool Suite. www.cs.utexas.edu/users/schwartz/ATS.html.
• 10: Scaling Step-Wise Refinement, IEEE Transactions on Software Engineering, v.30 n.6, p.355-371, June 2004 [doi>10.1109/TSE.2004.23]
• 11: D. Batory. "Feature Models, Grammars, and Propositional Formulas", Software Product Line Conference (SPLC), September 2005.
• 12: D. Batory, Multilevel models in model-driven engineering, product lines, and metaprogramming, IBM Systems Journal, v.45 n.3, p.527-539, July 2006
• 13: P. Clements. private correspondence 2005.
• 14: A. Colyer, A. Rashid, G. Blair. "On the Separation of Concerns in Program Families". Technical Report COMP-001-2004, Lancaster University, 2004.
• 15: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 16: Krzysztof Czarnecki , Ulrich W. Eisenecker, Generative programming: methods, tools, and applications, ACM Press/Addison-Wesley Publishing Co., New York, NY, 2000
• 17: Krzysztof Czarnecki , Krzysztof Pietroszek, Verifying feature-based model templates against well-formedness OCL constraints, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA [doi>10.1145/1173706.1173738]
• 18: Thomas R. Dean , David A. Lamb, A theory model core for module interconnection languages, Proceedings of the 1994 conference of the Centre for Advanced Studies on Collaborative research, p.13, October 31-November 03, 1994, Toronto, Ontario, Canada
• 19: Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, Classes and mixins, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268961]
• 20: Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, A Programmer's Reduction Semantics for Classes and Mixins, Formal Syntax and Semantics of Java, p.241-269, January 1999
• 21: Kenneth D. Forbus , Johan de Kleer, Building problem solvers, MIT Press, Cambridge, MA, 1993
• 22: Refactoring: improving the design of existing code, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 23: Irum Godil , Hans-Arno Jacobsen, Horizontal decomposition of Prevayler, Proceedings of the 2005 conference of the Centre for Advanced Studies on Collaborative research, p.83-100, October 17-20, 2005, Toranto, Ontario, Canada
• 24: Jack Greenfield , Keith Short , Steve Cook , Stuart Kent, Software Factories: Assembling Applications with Patterns, Models, Frameworks, and Tools, John Wiley & Sons, 2004
• 25: Ian M. Holland, Specifying Reusable Components Using Contracts, Proceedings of the European Conference on Object-Oriented Programming, p.287-308, June 29-July 03, 1992
• 26: S. S. Huang, D. Zook, and Y. Smaragdakis. "Statically Safe Program Generation with SafeGen", GPCE 2005.
• 27: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 28: M. de Jong and J. Visser. "Grammars as Feature Diagrams". www.cs.uu.nl/wiki/Merijn/PaperGrammarsAsFeatureDiagrams,2002.
• 29: K. Kang, S. Cohen, J. Hess, W. Nowak, and S. Peterson. "Feature-Oriented Domain Analysis (FODA) Feasibility Study". Technical Report, CMU/SEI-90TR-21, Nov. 1990.
• 30: K. Kang. private communication, 2005.
• 31: Günter Kniesel, Type-Safe Delegation for Run-Time Component Adaptation, Proceedings of the 13th European Conference on Object-Oriented Programming, p.351-366, June 14-18, 1999
• 32: Eugene Kohlbecker , Daniel P. Friedman , Matthias Felleisen , Bruce Duba, Hygienic macro expansion, Proceedings of the 1986 ACM conference on LISP and functional programming, p.151-161, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319859]
• 33: Kathi Fisler , Shriram Krishnamurthi, Modular verification of collaboration-based software designs, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 34: Shriram Krishnamurthi , Kathi Fisler , Michael Greenberg, Verifying aspect advice modularly, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 35: Vinay Kulkarni , Sreedhar Reddy, Separation of Concerns in Model-Driven Development, IEEE Software, v.20 n.5, p.64-69, September 2003 [doi>10.1109/MS.2003.1231154]
• 36: Roberto E. Lopez-Herrejon , Don S. Batory, A Standard Problem for Evaluating Product-Line Methodologies, Proceedings of the Third International Conference on Generative and Component-Based Software Engineering, p.10-24, September 09-13, 2001
• 37: R. E. Lopez-Herrejon and D. Batory. "Using Hyper/J to implement Product Lines: A Case Study", Dept. Computer Sciences, Univ. Texas at Austin, 2002.
• 38: Jia Liu , Don Batory , Christian Lengauer, Feature oriented refactoring of legacy applications, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134303]
• 39: C. McManus, The Basics of Java Class Loaders, www.javaworld.com/javaworld/jw-10-1996/jw-10-indepth.html
• 40: M. Odersky, et al. An Overview of the Scala Programming Language. September (2004), scala.epfl.ch
• 41: H. Ossher and P. Tarr. "Multi-dimensional Separation of Concerns and the Hyperspace Approach." In Software Architectures and Component Technology, Kluwer, 2002.
• 42: D. L. Parnas, On the Design and Development of Program Families, IEEE Transactions on Software Engineering, v.2 n.1, p.1-9, January 1976 [doi>10.1109/TSE.1976.233797]
• 43: Klaus Pohl , Günter Böckle , Frank J. van der Linden, Software Product Line Engineering: Foundations, Principles and Techniques, Springer-Verlag New York, Inc., Secaucus, NJ, 2005
• 44: Prevaler Project. www.prevayler.org/.
• 45: Ruben Prieto-Diaz , James M Neighbors, Module interconnection languages, Journal of Systems and Software, v.6 n.4, p.307-334, Nov. 1986 [doi>10.1016/0164-1212(86)90002-6]
• 46: SAT4J Satisfiability Solver, www.sat4j.org/
• 47: Mary Shaw , David Garlan, Software architecture: perspectives on an emerging discipline, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 48: Specware. www.specware.org.
• 49: R. Strnisza and M. Parkinson, "Lightweight Java: A Fully-Formalized, Extensible Minimal Imperative Fragment of Java", http://www.cl.cam.ac.uk/~rs456/lj/
• 50: Janos Sztipanovits , Gabor Karsai, Model-Integrated Computing, Computer, v.30 n.4, p.110-111, April 1997 [doi>10.1109/2.585163]
• 51: Walid Taha , Tim Sheard, Multi-stage programming with explicit annotations, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.203-217, June 12-13, 1997, Amsterdam, The Netherlands
• 52: S. Thaker. "Design and Analysis of Multidimensional Program Structures", M. Sc. Thesis, Department of Computer Sciences, The University of Texas at Austin, 2006.
• 53: Michael VanHilst , David Notkin, Using C++ Templates to Implement Role-Based Designs, Proceedings of the Second JSSST International Symposium on Object Technologies for Advanced Software, p.22-37, March 11-15, 1996
• 54: Eric G. Wagner, Algebraic specifications: some old history and new thoughts, Nordic Journal of Computing, v.9 n.4, p.373-404, Winter 2002
• 55: Niklaus Wirth, Program development by stepwise refinement, Communications of the ACM, v.14 n.4, p.221-227, April 1971 [doi>10.1145/362575.362577]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Data abstraction; Languages (e.g., description, interconnection, definition)
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers

General Terms:
Design, Languages, Verification

Keywords:
SAT solvers, compositional programming, features, product lines