Model-based development of dynamically adaptive software

ABSTRACT

Increasingly, software should dynamically adapt its behavior at run-time in response to changing conditions in the supporting computing and communication infrastructure, and in the surrounding physical environment. In order for an adaptive program to be trusted, it is important to have mechanisms to ensure that the program functions correctly during and after adaptations. Adaptive programs are generally more difficult to specify, verify, and validate due to their high complexity. Particularly, when involving multi-threaded adaptations, the program behavior is the result of the collaborative behavior of multiple threads and software components. This paper introduces an approach to create formal models for the behavior of adaptive programs. Our approach separates the adaptation behavior and non-adaptive behavior specifications of adaptive programs, making the models easier to specify and more amenable to automated analysis and visual inspection. We introduce a process to construct adaptation models, automatically generate adaptive programs from the models, and verify and validate the models. We illustrate our approach through the development of an adaptive GSM-oriented audio streaming protocol for a mobile computing application.

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: Jeremy S. Bradbury , James R. Cordy , Juergen Dingel , Michel Wermelinger, A survey of self-management in dynamic software architecture specifications, Proceedings of the 1st ACM SIGSOFT workshop on Self-managed systems, p.28-33, October 31-November 01, 2004, Newport Beach, California [doi>10.1145/1075405.1075411]
• 3: Daniel Le Métayer, Software architecture styles as graph grammars, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.15-23, October 16-18, 1996, San Francisco, California, United States
• 4: Gabriele Taentzer , Michael Goedicke , Torsten Meyer, Dynamic Change Management by Distributed Graph Transformation: Towards Configurable Distributed Systems, Selected papers from the 6th International Workshop on Theory and Application of Graph Transformations, p.179-193, November 16-20, 1998
• 5: Dan Hirsch , Paolo Inverardi , Ugo Montanari, Graph grammars and constraint solving for software architecture styles, Proceedings of the third international workshop on Software architecture, p.69-72, November 01-05, 1998, Orlando, Florida, United States [doi>10.1145/288408.288426]
• 6: 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
• 7: Richard N. Taylor , Nenad Medvidovic , Kenneth M. Anderson , E. James Whitehead, Jr. , Jason E. Robbins, A component- and message-based architectural style for GUI software, Proceedings of the 17th international conference on Software engineering, p.295-304, April 24-28, 1995, Seattle, Washington, United States [doi>10.1145/225014.225042]
• 8: 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]
• 9: R. Allen, R. Douence, and D. Garlan, "Specifying and analyzing dynamic software architectures," in Proceedings of the 1998 Conference on Fundamental Approaches to Software Engineering (FASE'98)(Lisbon, Portugal), March 1998.
• 10: J. Kramer , J. Magee, Analysing Dynamic Change in Software Architectures: A Case Study, Proceedings of the International Conference on Configurable Distributed Systems, p.91, March 04-06, 1998
• 11: Carlos Canal , Ernesto Pimentel , José M. Troya, Specification and Refinement of Dynamic Software Architectures, Proceedings of the TC2 First Working IFIP Conference on Software Architecture (WICSA1), p.107-126, February 22-24, 1999
• 12: Z. Zhou, P. K. McKinley, and S. M. Sadjadi, "On quality-of-service and energy consumption tradeoffs in fec-encoded wireless audio streaming," in Proceedings of the 12th IEEE International Workshop on Quality of Service (IWQoS 2004) (Montreal, Canada), June 2004. best paper award.
• 13: C. A. Petri, Kommunikation mit A utomaten PhDthesis, Sehriften des Institutes flir instrumentelle Mathematik, Bonn, Germany, 1962.
• 14: James L. Peterson, Petri Nets, ACM Computing Surveys (CSUR), v.9 n.3, p.223-252, Sept. 1977 [doi>10.1145/356698.356702]
• 15: Marko Mäkelä, Maria: Modular Reachability Analyser for Algebraic System Nets, Proceedings of the 23rd International Conference on Applications and Theory of Petri Nets, p.434-444, June 24-30, 2002
• 16: O. Kummer and F. Wienberg, "Renew--the reference net workshop," in In Tool Demonstrations, 21st International Conference on Application and Theory of Petri Nets (Aarhus, Denmark), pp. 28--30, 2000.
• 17: J.--C. Bolot and A. Vega-Garcia, "Control mechanisms for packet audio in the internet," in Proceedings of IEEE INFO-COM96 (San Francisco, California), pp. 232--239, 1996.
• 18: 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]
• 19: D. M. Berry, B. H. Cheng, and J. Zhang, "The four levels of requirements engineering for and in dynamic adaptive systems," in Proc. of 11th International Workshop on Requirements Engineering: Foundation for Software Quality (Porto, Portugal), June 2005.
• 20: Ji Zhang , Betty H. C. Cheng, Specifying adaptation semantics, Proceedings of the 2005 workshop on Architecting dependable systems, p.1-7, May 17-17, 2005, St. Louis, Missouri
• 21: Alexei Lapouchnian , Sotirios Liaskos , John Mylopoulos , Yijun Yu, Towards requirements-driven autonomic systems design, Proceedings of the 2005 workshop on Design and evolution of autonomic application software, May 21-21, 2005, St. Louis, Missouri
• 22: Axel van Lamsweerde, Goal-Oriented Requirements Engineering: A Guided Tour, Proceedings of the 5th IEEE International Symposium on Requirements Engineering, p.249, August 27-31, 2001
• 23: 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
• 24: J. Zhang and B. H. Cheng, "Model-based development of dynamically adaptive software," Tech. Rep. MSU-CSE-05-24, Computer Science and Engineering, Michigan State University, East Lansing, Michigan, September 2005.
• 25: Howard Bowman , Simon Thompson, A Tableau Method for Interval Temporal Logic with Projection, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, p.108-123, May 05-08, 1998
• 26: Alexander Pretschner, Model-based testing, Proceedings of the 27th international conference on Software engineering, p.722-723, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062636]
• 27: Ben Potter , Jane Sinclair , David Till, An introduction to formal specification and Z, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 28: James Rumbaugh , Ivar Jacobson , Grady Booch, The Unified Modeling Language reference manual, Addison-Wesley Longman Ltd., Essex, UK, 1998
• 29: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 30: "RAPIDware." http://www. cse. msu. edu/rapidware/.
• 31: 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.
• 32: 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.
• 33: S. Kulkarni and K. Biyani, "Correctness of component-based adaptation," in Proceedings of International Symposium on Component-based Software Engineering May 2004.
• 34: Constructing Adaptive Software in Distributed Systems, Proceedings of the The 21st International Conference on Distributed Computing Systems, p.635, April 16-19, 2001
• 35: 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
• 36: 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
• 37: T. A. Henzinger, R. Jhala, R. Majumdar, and M. A. Sanvido, "Extreme model checking," Verification: Theory and Practice, Lecture Notes in Computer Science 2772, Springer-Verlag pp. 332--358, 2004.
• 38: M. Mäkelä, "Model checking safety properties in modular high-level nets," in Application and Theory of Petri Nets 2003, 24th International Conference, ICATPN 2003 (volume 2679 of Lecture Notes in Computer Science) (Eindhoven, The Netherlands), pp. 201--220, Springer-Verlag, June 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking; Validation; Reliability

General Terms:
Design, Reliability, Verification

Keywords:
autonomic computing, dynamic adaptation, formal specification, global invariants, reliability, verification