LOVER: Light-weight Formal Verification of adaptivE systems at Run time

Adaptive systems are able to modify their behaviors to re- spond to significant changes at run time such as component failures. In many cases, run-time adaptation is simply replacing a piece of system with a new one without interrupting the system operation. In terms of component-based systems, an adaptation may be defined as replacing a system component with a new version at run time. However, updating a system with new components requires the assurance that the new config- uration will fully satisfy the expected requirements. Formal verification has been widely used to guarantee that a system specification satisfies a set of properties. However, applying verification techniques at run time for any potential change can be very expensive and sometimes unfeasible. In this paper, we present a methodology, called LOVER, for the lightweight verification of component-based adaptive systems. LOVER provides a new process model supported with formalisms, verification algorithms and tool to verify a significant subset of CTL properties.