摘要
研究使用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.
出处
《软件学报》
EI
CSCD
北大核心
2002年第5期913-920,共8页
Journal of Software
基金
国家863高科技发展计划资助项目(863-306-ZT02-04-01)
国家九五重点科技攻关项目(98-780-01-07-01)~~
关键词
验证
容错系统
时序逻辑语言
XYZ/E语言
软件系统
fault-tolerant system
temporal logic language XYZ/E
refinement
fault-tolerant transformation
specification
verification
