%0 Journal Article
%T Specification and Verification of the Triple-Modular Redundancy Fault-Tolerant System<br>三机冗余容错系统的描述和验证
%A GUO Liang
%A TANG Zhi-Song
%A <br>郭亮
%A 唐稚松
%J 软件学报
%D 2003
%I 
%X XYZ/E is used to specify and verify the triple-modular redundancy fault-tolerant system. Assuming that each computer is loaded with a determined sequential program P which continuously outputs data to the outer environment, the case P running on single processor is illustrated by an XYZ/E program SingleProcessP, and the property of program P is specified by a temporal logical formula SpecP. Finally, it is proved that the program TripleProcessorsP obtained from the triple-modular redundancy way can still satisfy SpecP in spite of hardware errors.
%K temporal logic language XYZ/E
%K fault-tolerant system
%K triple-modular redundancy
%K specification
%K verification<br>时序逻辑语言XYZ/E
%K 容错系统
%K 三机冗余
%K 描述
%K 验证
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=52F2044C2B8640E6&yid=D43C4A19B2EE3C0A&vid=F3583C8E78166B9E&iid=CA4FD0336C81A37A&sid=318E4CC20AED4940&eid=1D0FA33DA02ABACD&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=10