| 三机冗余容错系统的描述和验证 |
| |
| 引用本文： | 郭亮,唐稚松.三机冗余容错系统的描述和验证[J].软件学报,2003,14(1):54-61. |
| |
| 作者姓名： | 郭亮 唐稚松 |
| |
| 作者单位： | 中国科学院,软件研究所,计算机科学重点研究实验室,北京,100080 |
| |
| 基金项目： | (国家自然科学基金)No.60073020，(国家863高科技发展计划)No.863-306-ZT02-04-01 ~ |
| |
| 摘 要： | 使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessorP刻画程序P在单机上运行,用时序逻辑式SpecP刻画P向外部环境输出的数据所满足的性质.最后证明,采用三机冗余模式所得到的程序TripleProcessorsP即使在出现硬件错误的情况下运行,也能满足性质SpecP.
|
| 关 键 词： | 时序逻辑语言XYZ/E 容错系统 三机冗余 描述 验证 |
| 文章编号： | 1000-9825/2003/14(01)0054 |
| 收稿时间： | 2001/7/31 0:00:00 |
| 修稿时间： | 2001年7月31日 |
Specification and Verification of the Triple-Modular Redundancy Fault-Tolerant System |
| |
| GUO Liang and TANG Zhi-Song.Specification and Verification of the Triple-Modular Redundancy Fault-Tolerant System[J].Journal of Software,2003,14(1):54-61. |
| |
| Authors: | GUO Liang and TANG Zhi-Song |
| |
| 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. |
| |
| Keywords: | temporal logic language XYZ/E fault-tolerant system triple-modular redundancy specification verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
