Modular verification of dynamically adaptive systems

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 highassurance 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 to LTL) to concisely specify properties that hold during the adaptation process. Model checking offers an attractive approach to au...

• Type: Conference
• Year: 2009
• Where: AOSD
• Authors: Ji Zhang, Heather Goldsby, Betty H. C. Cheng
• Keywords: Adaptive Program, AOSD 2009, Model Checking, Software Engineering, Steady-state Programs