软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2003年
1期
54-61
,共8页
时序逻辑语言XYZ/E%容错系统%三机冗余%描述%验证
時序邏輯語言XYZ/E%容錯繫統%三機冗餘%描述%驗證
시서라집어언XYZ/E%용착계통%삼궤용여%묘술%험증
使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessorP刻画程序P在单机上运行,用时序逻辑式SpecP刻画P向外部环境输出的数据所满足的性质.最后证明,采用三机冗余模式所得到的程序TripleProcessorsP即使在出现硬件错误的情况下运行,也能满足性质SpecP.
使用XYZ/E描述和驗證三機冗餘容錯繫統.攷慮每檯計算機加載瞭一箇不斷嚮外界環境輸齣數據的確定性順序程序P,用XYZ/E程序SingleProcessorP刻畫程序P在單機上運行,用時序邏輯式SpecP刻畫P嚮外部環境輸齣的數據所滿足的性質.最後證明,採用三機冗餘模式所得到的程序TripleProcessorsP即使在齣現硬件錯誤的情況下運行,也能滿足性質SpecP.
사용XYZ/E묘술화험증삼궤용여용착계통.고필매태계산궤가재료일개불단향외계배경수출수거적학정성순서정서P,용XYZ/E정서SingleProcessorP각화정서P재단궤상운행,용시서라집식SpecP각화P향외부배경수출적수거소만족적성질.최후증명,채용삼궤용여모식소득도적정서TripleProcessorsP즉사재출현경건착오적정황하운행,야능만족성질SpecP.
