%0 Journal Article
%T To Specify and Verify Fault-Tolerant Systems in XYZ/E<br>基于XYZ/E描述和验证容错系统
%A GUO Liang
%A TANG Zhi-song
%A <br>郭亮
%A 唐稚松
%J 软件学报
%D 2002
%I 
%X 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.
%K fault-tolerant system
%K temporal logic language XYZ/E
%K refinement
%K fault-tolerant transformation
%K specification
%K verification<br>容错系统
%K 时序逻辑语言XYZ/E
%K 求精
%K 容错转换
%K 规范
%K 验证
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=D5EB4F23CCD6C10B&yid=C3ACC247184A22C1&vid=FC0714F8D2EB605D&iid=94C357A881DFC066&sid=8637B749179B02B3&eid=753F7A67351FADCC&journal_id=1000-9825&journal_name=软件学报&referenced_num=2&reference_num=10