Modeling and Customization of Fault Tolerant Architecture using Object-Z/XVCL

This paper proposes a novel heterogeneous software architecture FTA (fault tolerant architecture). FTA incorporates idealized fault tolerant component concept and coordinated error recovery mechanism in the early system design phase. It can be reused in the high level model design of specific mission critical distributed systems with reliability requirements. The formal model of FTA in the Object-Z language is presented to provide precise idioms to the system designers. Formal proof using the Object-Z reasoning rules are constructed to demonstrate the fault tolerant properties of FTA. By analyzing the customization process, we also present a FTA template, expressed in x-frames using XVCL (XML-based variant configuration language) methodology, to automate the customization process. We apply a sales control system case study to illustrate the customization of FTA.