Modular verification of dynamically adaptive systems

ABSTRACT

Cyber-physical systems increasingly rely on dynamically adaptive programs to respond to changes in their physical environment; examples include ecosystem monitoring and disaster relief systems. These systems are considered high-assurance since errors during execution could result in injury, loss of life, environmental impact, and/or financial loss. In order to facilitate the development and verification of dynamically adaptive systems, we separate functional concerns from adaptive concerns. Specifically, we model a dynamically adaptive program as a collection of (non-adaptive) steady-state programs and a set of adaptations that realize transitions among steady state programs in response to environmental changes. We use Linear Temporal Logic (LTL) to specify properties of the non-adaptive portions of the system, and we use A-LTL (an adapt-operator extension toLTL) to concisely specify properties that hold during the adaptation process. Model checking offers an attractive approach to automatically analyzing models for adherence to formal properties and thus providing assurance. However, currently, model checkers are unable to verify properties specified using A-LTL. Moreover, as the number of steady-state programs and adaptations increase, the verification costs (in terms of space and time) potentially become unwieldy. To address these issues, we propose a modular model checking approach to verifying that a formal model of an adaptive program satisfies its requirements specified in LTL and A-LTL, respectively.

REFERENCES

• 1: 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.
• 2: Rajeev Alur , Mihalis Yannakakis, Model checking of hierarchical state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.273-303, May 2001 [doi>10.1145/503502.503503]
• 3: 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
• 4: 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
• 5: Constructing Adaptive Software in Distributed Systems, Proceedings of the The 21st International Conference on Distributed Computing Systems, p.635, April 16-19, 2001
• 6: B. H. C. Cheng, H. J. Goldsby, and J. Zhang. Amoeba-RT: Run-time verification of adaptive software. In In Holger Giese, editor, Models in Software Engineering Workshops and Symposia at MoDELS 2007, Nashville, TN, USA, October 2007. Springer Verlag.
• 7: C. Clifton and G. T. Leavens. Observers and assistants: A proposal for modular aspect-oriented reasoning. In In Foundations of Aspect Languages, pages 33--44, 2002.
• 8: Jamieson M. Cobleigh , George S. Avrunin , Lori A. Clarke, Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146250]
• 9: C. Courcoubetis , M. Vardi , P. Wolper , M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design, v.1 n.2-3, p.275-288, Oct. 1992 [doi>10.1007/BF00121128]
• 10: E. Allen Emerson , Joseph Y. Halpern, Decision procedures and expressiveness in the temporal logic of branching time, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.169-180, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802190]
• 11: 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
• 12: C. Flanagan and S. Qadeer. Thread--modular model checking. In SPIN 03: SPIN Workshop, LNCS 2648, pages 213--225. Springer-Verlag, 2003.
• 13: Brent Hailpern , Susan Owicki, Modular verification of concurrent programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.322-336, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582187]
• 14: K. Havelund and G. Rosu. Monitoring Java programs with Java PathExplorer. In Proceedings of the 1st Workshop on Runtime Verification, Paris, France, July 2001.
• 15: T. A. Henzinger, R. Jhala, R. Ma jumdar, and M. A. Sanvido. Extreme model checking. Verification: Theory and Practice, Lecture Notes in Computer Science 2772, Springer-Verlag, pages 332--358, 2004.
• 16: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 17: C. B. Jones, Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.4, p.596-619, Oct. 1983 [doi>10.1145/69575.69577]
• 18: Bengt Jonsson , Yih-Kuen Tsay, Assumption/guarantee specifications in linear-time temporal logic, Theoretical Computer Science, v.167 n.1-2, p.47-72, Oct. 30, 1996
• 19: 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
• 20: 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
• 21: S. Kulkarni and K. Biyani. Correctness of component-based adaptation. In Proceedings of International Symposium on Component-based Software Engineering, May 2004.
• 22: Orna Kupferman , Moshe Y. Vardi, Modular Model Checking, Revised Lectures from the International Symposium on Compositionality: The Significant Difference, p.381-401, September 08-12, 1997
• 23: Harry Li , Shriram Krishnamurthi , Kathi Fisler, Verifying cross-cutting features as open systems, ACM SIGSOFT Software Engineering Notes, v.27 n.6, November 2002 [doi>10.1145/605466.605481]
• 24: 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]
• 25: Barbara Liskov, Abstraction and specification in program development, MIT Press, Cambridge, MA, 1986
• 26: Jeff Magee, Behavioral analysis of software architectures using LTSA, Proceedings of the 21st international conference on Software engineering, p.634-637, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302726]
• 27: P. K. McKinley. RAPIDware. http://www.cse.msu.edu/rapidware/. Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan State Computer Science and Engineering, Michigan State
• 28: D. L. Parnas, On the criteria to be used in decomposing systems into modules, Communications of the ACM, v.15 n.12, p.1053-1058, Dec. 1972 [doi>10.1145/361598.361623]
• 29: Amir Pnueli, The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, p.46-57, September 30-October 31, 1977
• 30: M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the 1st Symposium on Logic in Computer Science, pages 322--331, Cambridge, England, 1986.
• 31: Ji Zhang , Betty H. C. Cheng, Model-based development of dynamically adaptive software, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134337]
• 32: J. Zhang and B. H. C. Cheng. Modular model checking of dynamically adaptive programs. Technical Report MSU-CSE-06-18, Computer Science and Engineering, Michigan State University, East Lansing, Michigan, March 2006. http://www.cse.msu.edu/ hjg/Zhang06Modular.pdf.
• 33: J. Zhang and B. H. C. Cheng. Using temporal logic to specify adaptive program semantics. Journal of Systems and Software (JSS), Architecting Dependable Systems, 79(10):1361--1369, 2006.
• 34: J. Zhang, B. H. C. Cheng, Z. Yang, and P. K. McKinley. Enabling safe dynamic component-based software adaptation. Architecting Dependable Systems, Lecture Notes in Computer Science, pages 194--211, 2005.

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: Reliability; Model checking; Validation

General Terms:
Design, Reliability, Verification

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