Towards compositional synthesis of evolving systems

ABSTRACT

Synthesis of system configurations from a given set of features is an important and very challenging problem. This paper makes a step towards this goal by describing an efficient technique for synthesizing pipeline configurations of feature-based systems. We identify and formalize a design pattern that is commonly used in featurebased development. We show that this pattern enables compositional synthesis of feature arrangements. In particular, the pattern allows us to add or remove features from an existing system without having to reconfigure the system from scratch. We describe an implementation of our technique and evaluate its applicability and effectiveness using a set of telecommunication features from AT&T, arranged within the DFC architecture.

REFERENCES

• 1: Don Batory, Feature-Oriented Programming and the AHEAD Tool Suite, Proceedings of the 26th International Conference on Software Engineering, p.702-703, May 23-28, 2004
• 2: Aysu Betin-Can , Tevfik Bultan , Mikael Lindvall , Benjamin Lux , Stefan Topp, Application of design for verification with concurrency controllers to air traffic control software, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101914]
• 3: J. Blom, B. Jonsson, and L. Kempe. "Using Temporal Logic for Modular Specification of Telephone Services". In Proceedings of FIW'94, pages 197--216, 1994.
• 4: K. Braithwaite and J. Atlee. "Towards Automated Detection of Feature Interactions". In Proceedings of FIW'94, pages 36--59, 1994.
• 5: Daniel Brand , Pitro Zafiropulo, On Communicating Finite-State Machines, Journal of the ACM (JACM), v.30 n.2, p.323-342, April 1983 [doi>10.1145/322374.322380]
• 6: R. Brooks. "A Robust Layered Control System for a Mobile Robot". IEEE J. of Robotics and Automation, pages 2--27, 1986.
• 7: G. Bruns. "Foundations for Features". In Proceedings of FIW'05, pages 3--11, 2005.
• 8: B. Cheng, R. Stephenson, and B. Berenbach. "Lessons Learned from Automated Analysis of Industrial UML Class Models (An Experience Report)". In Proceedings of MoDELS'05, pages 324--338, 2005.
• 9: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 10: J. Cobleigh, D. Giannakopoulou, and C. Pasareanu. "Learning Assumptions for Compositional Verification". In Proceedings of TACAS'03, pages 331--346, 2003.
• 11: Alma L. Juarez Dominguez , Nancy A. Day, Compositional reasoning for port-based distributed systems, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101974]
• 12: E. Allen Emerson , Vineet Kahlon, Reducing Model Checking of the Many to the Few, Proceedings of the 17th International Conference on Automated Deduction, p.236-254, June 17-20, 2000
• 13: E. Allen Emerson , Kedar S. Namjoshi, Reasoning about rings, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-94, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199468]
• 14: Amy P. Felty , Kedar S. Namjoshi, Feature specification and automated conflict detection, ACM Transactions on Software Engineering and Methodology (TOSEM), v.12 n.1, p.3-27, January 2003 [doi>10.1145/839268.839270]
• 15: K. Fisler and S. Krishnamurthi. "Decomposing Verification by Features". In Proceedings of VSTTE'05, 2005.
• 16: Xiang Fu , Tevfik Bultan , Jianwen Su, Analysis of interacting BPEL web services, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA [doi>10.1145/988672.988756]
• 17: Robert J. Hall, Feature combination and interaction detection via foreground/background models, Computer Networks: The International Journal of Computer and Telecommunications Networking, v.32 n.4, p.449-469, April 2000 [doi>10.1016/S1389-1286(00)00010-4]
• 18: W. Harrison, H. Ossher, P. Tarr, V. Kruskal, and F. Tip. "CAT: A toolkit for assembling concerns". Technical Report RC22686, IBM Research, 2002.
• 19: Jonathan D. Hay , Joanne M. Atlee, Composing features and resolving interactions, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.110-119, November 06-10, 2000, San Diego, California, United States
• 20: Daniel Jackson, Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
• 21: Michael Jackson , Pamela Zave, Distributed Feature Composition: A Virtual Architecture for Telecommunications Services, IEEE Transactions on Software Engineering, v.24 n.10, p.831-847, October 1998 [doi>10.1109/32.729683]
• 22: F. Laburthe and N. Jussien. "The Choco Constraint Programming System". http://choco-solver.net/.
• 23: Kim Guldstrand Larsen , Bernhard Steffen , Carsten Weise, A Constraint Oriented Proof Methodology Based on Modal Transition Systems, Proceedings of the First International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.17-40, May 19-20, 1995
• 24: Harry Li , Shriram Krishnamurthi , Kathi Fisler, Verifying cross-cutting features as open systems, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587066]
• 25: Harry C. Li , Shriram Krishnamurthi , Kathi Fisler, Modular Verification of Open Features Using Three-Valued Model Checking, Automated Software Engineering, v.12 n.3, p.349-382, July 2005 [doi>10.1007/s10515-005-2643-9]
• 26: Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]
• 27: Jeff Magee, Concurrency: State Models And Java Programs, John Wiley & Sons, 2006
• 28: Peter C. Mehlitz , John Penix, Design for Verification with Dynamic Assertions, Proceedings of the 29th Annual IEEE/NASA on Software Engineering Workshop, p.285-292, April 06-07, 2005 [doi>10.1109/SEW.2005.23]
• 29: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 30: S. Nejati. "Translating BoxTalk Models to I/O Automata", 2007. http://www.cs.toronto.edu/~shiva/synthesis/.
• 31: Malte Plath , Mark Ryan, Feature integration using a feature construct, Science of Computer Programming, v.41 n.1, p.53-84, September 2001 [doi>10.1016/S0167-6423(00)00018-6]
• 32: A. Pnueli, In transition from global to modular temporal reasoning about programs, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 33: Keith P. Pomakis , Joanne M. Atlee, Reachability analysis of feature interactions: a progress report, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.216-223, January 08-10, 1996, San Diego, California, United States
• 34: C. Prehofer. "Feature-Oriented Programming: A Fresh Look at Objects". In Proceedings of ECOOP'97, pages 419--443, 1997.
• 35: Natasha Sharygina , James C. Browne , Robert P. Kurshan, A Formal Object-Oriented Analysis for Software Reliability: Design for Verification, Proceedings of the 4th International Conference on Fundamental Approaches to Software Engineering, p.318-332, April 02-06, 2001
• 36: Mary Shaw , David Garlan, Software architecture: perspectives on an emerging discipline, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 37: P. Zave. "FAQ Sheet on Feature Interaction". http://www.research.att.com/~pamela/faq.html.
• 38: P. Zave and M. Jackson. "A Call Abstraction for Component Coordination". Elect. Notes in Theor. CS, 66(4), 2002.
• 39: P. Ann Zimmer, Prioritizing features through categorization: an approach to resolving feature interactions, University of Waterloo, Waterloo, Ont., Canada, 2007

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

General Terms:
Design, Verification

Keywords:
I/O automata, behavioural design patterns, feature-based development, pipelines, synthesis