Concurrency and Complexity in Verifying Dynamic Adaptation: A Case Study?

Abstract. Software systems need to adapt as requirements change, en-vironment conditions vary, and bugs are discovered and xed. In systems that need to provide continuous operation, it is important that the adap-tation be done with minimal interruption in the execution of the system. In context of verication of these adaptive systems, the verication needs to be done for the system before adaptation, for the system during adapta-tion, and for the system after adaptation. While the existing techniques of program verication can be directly applied to verify the system before and the system after adaptation, they cannot be applied directly to verify the system during adaptation. This is because the system during adaptation is not well-dened as it consists of parts of both the old system (system before adaptation) and the new system (system after adaptation). In our previous work, we presented an approach based on adaptation lattice for verifying the correctness of dynamic adaptation. The complexity of our approach depends on the size (number of nodes and edges) of the adapta-tion lattice, as each node and each edge in the lattice needs to be veried independently. In this paper, we discuss the tradeo between concurrency of adaptation and complexity of verifying that adaptation.