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

Adaptive systems are able to modify their behaviors to re- spond to signicant 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 dened 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 conguration will fully satisfy the expected requirements. Formal verication has been widely used to guarantee that a system specication satises a set of properties. However, applying verication techniques at run time for any potential change can be very expensive and sometimes unfeasible. In this paper, we present a framework, called LOVER, for the lightweight verication of component-based adaptive systems at run time. LOVER provides a new process model supported with formalisms, verication algorithms and tool to verify a signicant subset of CTL properties.