###
DOI:
:2003.14(1):54-61

三机冗余容错系统的描述和验证
郭亮,唐稚松
(中国科学院,软件研究所,计算机科学重点研究实验室,北京,100080)
Specification and Verification of the Triple-Modular Redundancy Fault-Tolerant System
GUO Liang,TANG Zhi-Song
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 3096   Download 2772
Received:July 31, 2001    Revised:April 10, 2002
> 中文摘要: 使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessorP刻画程序P在单机上运行,用时序逻辑式SpecP刻画P向外部环境输出的数据所满足的性质.最后证明,采用三机冗余模式所得到的程序TripleProcessorsP即使在出现硬件错误的情况下运行,也能满足性质SpecP.
Abstract: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.
文章编号:     中图分类号:    文献标志码:
基金项目:
Foundation items:
Reference text:

郭亮,唐稚松.三机冗余容错系统的描述和验证.软件学报,2003,14(1):54-61

GUO Liang,TANG Zhi-Song.Specification and Verification of the Triple-Modular Redundancy Fault-Tolerant System.Journal of Software,2003,14(1):54-61