Concurrency and Complexity in Verifying Dynamic Adaptation: A Case Study

摘要

Software systems need to adapt as requirements change, environment conditions vary, and bugs are discovered and fixed. In systems that need to provide continuous operation, it is important that the adaptation be done with minimal interruption in the execution of the system. In context of verification of these adaptive systems, the verification needs to be done for the system before adaptation, for the system during adaptation, and for the system after adaptation. While the existing techniques of program verification 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-defined 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 adaptation lattice, as each node and each edge in the lattice needs to be verified independently. In this paper, we discuss the tradeoff between concurrency of adaptation and complexity of verifying that adaptation.