Verifying and Analyzing Adaptive Logic through UML State Models

It is becoming increasingly important to be able to adapt an application´s behavior at run time in response to changing requirements and environmental conditions. Adaptive programs are typically difficult to specify, design, and verify. A variety of conditions may trigger an adaptation, each of which may involve different types of adaptation mechanisms. In many cases, adaptive systems are concurrent, thus further exacerbating the complexity. Furthermore, it is important that adaptations do not put the system into an inconsistent state during or after adaptation. This paper presents an iterative approach to modeling and analyzing UML behavioral design models of adaptive systems, where the UML state diagrams are automatically translated into Promela code for analysis with the Spin model checker. The adaptive models are analyzed for adherence to both system invariants and properties that should hold during adaptation. We demonstrate this approach on applications for the mobile computing domain where we verify the design models against formally-specified properties.