基于XYZ/E描述和验证容错系统  

To Specify and Verify Fault-Tolerant Systems in XYZ/E

作　　者：郭亮[1] 唐稚松[1] 

机构地区：[1]中国科学院软件研究所计算机科学重点实验室,北京100080

出　　处：《软件学报》2002年第5期913-920,共8页Journal of Software

基　　金：国家863高科技发展计划资助项目(863-306-ZT02-04-01);国家九五重点科技攻关项目(98-780-01-07-01)~~

摘　　要：研究使用XYZ/E描述和验证容错系统.基于XYZ/E中可执行程序P对应的状态转换系统对其错误环境F建模,通过错误转换给出错误影响程序PF;基于P,F和恢复算法R,通过容错转换给出容错程序PF-R;定义了程序P,Q之间两种求精关系:容错求精和向后恢复求精,基于这两种求精关系可直接从程序P的规范推导出程序Q满足的一些性质.To specify and verify fault-tolerant systems in XYZ/E is discussed in this paper. Based on the corresponding state transition system of an XYZ/E executable program P, how to model its fault environment and obtain its fault affected program PF by fault transformation is illustrated. With P, F, PF and a recovery algorithm R, how to obtain the fault-tolerant program PF-R by fault tolerant transformation is also illustrated. Furthermore, two kinds of refinement relationships between programs P and Q: fault-tolerant refinement and backward-recovery refinement are defined. Based on these two refinement relationships, some properties satisfied by program Q can be directly deduced from the specification of program P.

关 键 词：验证 容错系统 时序逻辑语言 XYZ/E语言 软件系统 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]