Fault-Tolerant Online Backup Service: Formal Modeling and Reasoning

Online backup service software provides automated, offsite, secure online data backup and recovery for remote computers. How to satisfy functional requirements and guarantee the fault tolerance of online backup service software is a difficult but crucial problem faced by software designers. In this paper, we investigate to incorporate the fault tolerant techniques in the system design, and propose a fault-tolerant online backup service model (FOBSM) to guide the development of online backup service system. The FOBSM comprises four components: backup client (BC), backup server (BS), storage server (SS), and online backup exception handler (OBEH). The first three components constitute three-party functional units, whereas OBEH serves as the centralized exception handling mechanism, which is devised to receive the external exceptions raised by the other entities, transform them into a global exception, and propagate it to the related entities to handle, so as to improve the fault tolerance of the software greatly. In order to provide precise and explicit idioms to system designers, we use Object-Z language to specify the FOBSM. Following the Object-Z reasoning rules, we reason about the fault tolerant properties of FOBSM and demonstrate that it can improve fault tolerance of the online backup service software effectively.