Assurance of dynamic adaptation in distributed systems

Long running applications often need to adapt due to changing requirements or changing environment. Typically, such an adaptation is performed by dynamically adding or removing components. In these type of adaptations, components are often added to or removed from multiple processes in the system. As a result, during adaptation, the system may consist of both changed and unchanged processes, causing old and new components to overlap. This overlapping of components during adaptation may induce cross-component communication, which may lead to behavior during adaptation that is unpredictable and/or undesirable.In this paper, we discuss an approach to model and verify overlap adaptation. We use the transitional-invariant lattice and the transitional-faultspan lattice to verify the correctness of adaptation in the absence and the presence of faults, respectively. We also discuss a framework to support implementation of overlap adaptation.