To Specify and Verify Fault-Tolerant Systems in XYZ/E
基于XYZ/E描述和验证容错系统

To specify and verify fault-tolerant systems in XYZ/E is discussed in this paper. Based on the corresponding state transition system of an XYZ/E executable program P, how to model its fault environment and obtain its fault affected program PF by fault transformation is illustrated. With P, F, PF and a recovery algorithm R, how to obtain the fault-tolerant program PF-R by fault tolerant transformation is also illustrated. Furthermore, two kinds of refinement relationships between programs P and Q: fault-tolerant refinement and backward-recovery refinement are defined.Based on these two refinement realtionships,some properties satisfied by program Q can be directly deduced from the specification of programP.