Specifying adaptation semantics

ABSTRACT

Computer software must dynamically adapt to changing conditions. In order to fully realize the benefit of dynamic adaptation, it must be performed correctly. The correctness of adaptation cannot be properly addressed without precisely specifying the requirements for adaptation. This paper introduces an approach to formally specifying adaptation requirements in temporal logic. We introduce A-LTL, an adaptation-based extension to linear temporal logic, and use this logic to specify three commonly used adaptation semantics. Neighborhood composition and sequential composition techniques are developed and applied to A-LTL to construct the specification of an adaptive system. We introduce adaptation semantics graphs to visually present the adaptation semantics. Specifications for adaptive systems can be automatically generated from adaptation semantics graphs.

REFERENCES

• 1: Philip K. McKinley , Seyed Masoud Sadjadi , Eric P. Kasten , Betty H. C. Cheng, Composing Adaptive Software, Computer, v.37 n.7, p.56-64, July 2004 [doi>10.1109/MC.2004.48]
• 2: S. Kulkarni and K. Biyani, "Correctness of component-based adaptation," in Proceedings of International Symposium on Component-based Software Engineering, May 2004.
• 3: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, I, Information and Computation, v.100 n.1, p.1-40, Sept. 1992 [doi>10.1016/0890-5401(92)90008-4]
• 4: Jeff Kramer , Jeff Magee , Morris Sloman, Configuring distributed systems, Proceedings of the 5th workshop on ACM SIGOPS European workshop: Models and paradigms for distributed systems structuring, September 21-23, 1992, Mont Saint-Michel, France [doi>10.1145/506378.506406]
• 5: Carlos E. Cuesta , Pablo de la Fuente , Manuel Barrio-Solárzano, Dynamic coordination architecture through the use of reflection, Proceedings of the 2001 ACM symposium on Applied computing, p.134-140, March 2001, Las Vegas, Nevada, United States [doi>10.1145/372202.372298]
• 6: S. S. Kulkarni, K. N. Biyani, and U. Arumugam, "Composing distributed fault-tolerance components," in Proccedings of the International Conference on Dependable Systems and Networks (DSN), Supplemental Volume, Workshop on Principles of Dependable Systems, pp. W127--W136, June 2003.
• 7: Jeff Kramer , Jeff Magee, The Evolving Philosophers Problem: Dynamic Change Management, IEEE Transactions on Software Engineering, v.16 n.11, p.1293-1306, November 1990 [doi>10.1109/32.60317 ]
• 8: Peyman Oreizy , Nenad Medvidovic , Richard N. Taylor, Architecture-based runtime software evolution, Proceedings of the 20th international conference on Software engineering, p.177-186, April 19-25, 1998, Kyoto, Japan
• 9: Constructing Adaptive Software in Distributed Systems, Proceedings of the The 21st International Conference on Distributed Computing Systems, p.635, April 16-19, 2001
• 10: J. Appavoo , K. Hui , C. A. N. Soules , R. W. Wisniewski , D. M. Da Silva , O. Krieger , M. A. Auslander , D. J. Edelsohn , B. Gamsa , G. R. Ganger , P. McKenney , M. Ostrowski , B. Rosenburg , M. Stumm , J. Xenidis, Enabling autonomic behavior in systems software with hot swapping, IBM Systems Journal, v.42 n.1, p.60-76, January 2003
• 11: Noriki Amano , Takuo Watanabe, A software model for flexible & safe adaptation of mobile code programs, Proceedings of the International Workshop on Principles of Software Evolution, May 19-20, 2002, Orlando, Florida [doi>10.1145/512035.512050]
• 12: J. Zhang, Z. Yang, B. H. Cheng, and P. K. McKinley, "Adding safeness to dynamic adaptation techniques," in Proceedings of ICSE 2004 Workshop on Architecting Dependable Systems, (Edinburgh, Scotland, UK), May 2004.
• 13: J. Zhang, B. H. Cheng, Z. Yang, and P. K. McKinley, "Enabling safe dynamic component-based software adaptation," Architecting Dependable Systems, Lecture Notes in Computer Science, 2005. Accepted for publication.
• 14: A. Pnueli, "The temporal logic of programs," in Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46--57, 1977.
• 15: S. M. Sadjadi , P. K. McKinley , E. P. Kasten, Architecture and Operation of an Adaptable Communication Substrate, Proceedings of the The Ninth IEEE Workshop on Future Trends of Distributed Computing Systems (FTDCS'03), p.46, May 28-30, 2003
• 16: R. Rosner and A. Pnueli, "A choppy logic," in 1st IEEE Symposium on Logic in Computer Science, pp. 306--313, 1986.
• 17: J. Zhang and B. H. Cheng, "Adaptation semantics," Tech. Rep. MSU-CSE-05-7, Computer Science and Engineering, Michigan State University, East Lansing, Michigan, February 2005.
• 18: Matthew B. Dwyer , Corina S. Pasareanu, Filter-based model checking of partial systems, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.189-202, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 19: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 20: Rob Gerth , Doron Peled , Moshe Y. Vardi , Pierre Wolper, Simple on-the-fly automatic verification of linear temporal logic, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, p.3-18, June 01, 1995

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

General Terms:
Theory

Keywords:
adaptive software, autonomic computing, temporal logic