| 摘要: |
| 使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessorP刻画程序P在单机上运行,用时序逻辑式SpecP刻画P向外部环境输出的数据所满足的性质.最后证明,采用三机冗余模式所得到的程序TripleProcessorsP即使在出现硬件错误的情况下运行,也能满足性质SpecP. |
| 关键词: 时序逻辑语言XYZ/E 容错系统 三机冗余 描述 验证 |
| DOI： |
| 分类号: |
| 基金项目: |
|
| Specification and Verification of the Triple-Modular Redundancy Fault-Tolerant System |
|
GUO Liang,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. |
| Key words: temporal logic language XYZ/E fault-tolerant system triple-modular redundancy specification verification |
