Verifying Runtime Architectural Reconfiguration of Dynamically Adaptive Systems

Nowadays, dynamically adaptive systems are gaining more widespread use in several domains (mobile application, airports, banks, etc). These systems are often subject to evolution due to varying environmental conditions and the apparition of new user requirements. To maintain their usefulness, such systems must be always available and reliable. In this paper, we are particularly interested in the problem of managing and verifying runtime reconfigurations of dynamically adaptive systems. While managing runtime reconfigurations is achieved through the combination of the Aspect-Oriented Software Development (AOSD) and the Architecture Description Language (ADL), their verification is performed through checking the imposed architectural invariants on the whole application. For this purpose, we present how our approach supports runtime reconfigurations and how architectural invariants written in OCL language can be automatically translated into Schema Ron schemas and then how their preservation is verified to evaluate the runtime reconfigurations.