Formal Specification And Verification Of Automatic DMARF System

Nowadays, along with computing systems become more and more complex, there are more applications, servers and memorizers in the system which makes it even harder to manage efficiently. In order to keep reliability, our system needs to be self-managed.IBM raised Autonomic Computing technology in 2001, which is consisted of four main parts:self-protection, self-optimization, self-configuration and self-healing. Self-protection means that the system can protect itself from baleful attack and virus; Self-optimization predicates the system can reassign resources according to users' requirements in different time in order to keep efficient; Self-healing indicates the system can detect errors during runtime and recover by itself. Self-configuration means that the system can configure by itself, and change its configuration according to the environment dynamically.Autonomic Computing System achieves self-management by controlling the interactions between all the components, which is very hard to construct and command. How to build up a highly predictable and secure system? We can apply formal method to accomplish that. Communicating Sequential Processes (CSP) is a formal method, which describes the communications between components to simulate the features and activities of the whole system. CSP method plays an important role in depicting distributed and subsequent systems.In this paper, I take DMARF system as an example; describe self-protection, self-optimization and self-healing features using CSP method and provide the formal specification. Moreover, I use PAT tool to verify the autonomic features.