Sciweavers

Share
AOSD
2009
ACM

Modular verification of dynamically adaptive systems

9 years 5 months ago
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...
Ji Zhang, Heather Goldsby, Betty H. C. Cheng
Added 29 Sep 2010
Updated 29 Sep 2010
Type Conference
Year 2009
Where AOSD
Authors Ji Zhang, Heather Goldsby, Betty H. C. Cheng
Comments (0)
books