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

• 作者: 唐稚松 郭亮
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 时序逻辑语言XYZ/E 容错系统 三机冗余 描述 验证
• 年，卷（期）: 2003,（1）
• 所属期刊栏目: 系统软件与软件工程
• 页码范围: 54-61
• 页数: 8页
• 分类号: TP311
• 字数: 8388字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐稚松		7	188	6.0	7.0
2	郭亮		2	30	2.0	2.0