New Verification Approach for Reconfigurable Distributed Systems

Abstract

Adaptive systems are able to modify their behaviors to cope with unpredictable significant changes at run time such as component failures. These systems are critical for future project and other intelligent systems. Reconfiguration is often a major undertaking for systems: it might make its functions unavailable for some time and make potential harm to human life or large financial investments. Thus, updating a system with a new configuration requires the assurance that the new configuration 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 propose a new verification approach to deal with the formal verification of these reconfiguration scenarios. New reconfigurable CTL semantics is introduced to cover the verification of reconfigurable properties. It consists of two verification steps: design time and run time verification. A railway case study will be also presented.