Formal Recovery Analysis Approach for Service-Oriented System Based on Survivability Specification

From the perspective of service-oriented computing, a grid system is built by composing autonomous, loosely coupled and platform-independent services, whose dynamics and complexity bring great challenges to system survivability analysis. In the present of different kinds of malicious attacks, system failures or accidents, the system will provide a predefined survivability specification which consists of corresponding degraded services called service cores according to the application logic. How to formally describe the process and reason the properties of the recovery from one service core to another play an important role in analyzing system survivability. The main contributions of this paper are (1) presenting the method to represent service core based on component families and installation orders; (2) studying the success (the newly started services in the resulting service core function properly) and safety (the formerly started services in the starting service core are not damaged) properties of the recovery from one service core to another based on component compatibility and installation execution; (3) proposing the approach to simplify the component installation execution based on projection; (4) proposing a formal analysis approach for service-based system survivability based on survivability specification. The approach is applied in a simple service-based system called mobile video conference (MVC) to demonstrate its practicability and efficiency.