三机冗余容错系统的描述和验证

被引：4

作者：

郭亮

唐稚松

机构：

[1] 中国科学院软件研究所计算机科学重点研究实验室

[2] 中国科学院软件研究所计算机科学重点研究实验室北京

来源：

软件学报 | 2003年 / 01期

关键词：

时序逻辑语言XYZ/E; 容错系统; 三机冗余; 描述; 验证;

D O I：

10.13328/j.cnki.jos.2003.01.009

中图分类号：

TP302 [设计与性能分析];

学科分类号：

081201 ;

摘要：

使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessorP刻画程序P在单机上运行,用时序逻辑式SpecP刻画P向外部环境输出的数据所满足的性质.最后证明,采用三机冗余模式所得到的程序TripleProcessorsP即使在出现硬件错误的情况下运行,也能满足性质SpecP.

引用

页码：54 / 61

页数：8