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

郭亮; 唐稚松

引用本文:	郭亮,唐稚松.基于XYZ/E描述和验证容错系统.软件学报,2002,13(5):913-920

【打印本页】【下载PDF全文】【查看/发表评论】【EndNote】【RefMan】【BibTex】

←前一篇|后一篇→

过刊浏览高级检索

本文已被：浏览 3989次下载 6638次	码上扫一扫！
分享到：微信更多字体:加大+\|默认\|缩小-
基于XYZ/E描述和验证容错系统
郭亮¹, 唐稚松¹
中国科学院,软件研究所,计算机科学重点实验室,北京,100080

摘要:

研究使用XYZ/E描述和验证容错系统.基于XYZ/E中可执行程序P对应的状态转换系统对其错误环境F建模,通过错误转换给出错误影响程序P_F;基于P,F和恢复算法R,通过容错转换给出容错程序P_F-R;定义了程序P,Q之间两种求精关系:容错求精和向后恢复求精,基于这两种求精关系可直接从程序P的规范推导出程序Q满足的一些性质.

关键词: 容错系统时序逻辑语言XYZ/E 求精容错转换规范验证

DOI：

分类号:

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

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

GUO Liang,TANG Zhi-song

Abstract:

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 P_F by fault transformation is illustrated. With P, F, P_F and a recovery algorithm R, how to obtain the fault-tolerant program P_F-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 realtionships,some properties satisfied by program Q can be directly deduced from the specification of programP.

Key words: fault-tolerant system temporal logic language XYZ/E refinement fault-tolerant transformation specification verification