| 基于XYZ/E描述和验证容错系统 |
| |
| 引用本文： | 郭亮,唐稚松.基于XYZ/E描述和验证容错系统[J].软件学报,2002,13(5):913-920. |
| |
| 作者姓名： | 郭亮 唐稚松 |
| |
| 作者单位： | 中国科学院,软件研究所,计算机科学重点实验室,北京,100080 |
| |
| 基金项目： | 国家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满足的一些性质.
|
| 关 键 词： | 容错系统 时序逻辑语言XYZ/E 求精 容错转换 规范 验证 |
| 文章编号： | 1000-9825/2002/13(05)0913-08 |
| 收稿时间： | 2000/7/20 0:00:00 |
| 修稿时间： | 7/6/2001 12:00:00 AM |
To Specify and Verify Fault-Tolerant Systems in XYZ/E |
| |
| GUO Liang and TANG Zhi-song.To Specify and Verify Fault-Tolerant Systems in XYZ/E[J].Journal of Software,2002,13(5):913-920. |
| |
| Authors: | GUO Liang and 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 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 realtionships,some properties satisfied by program Q can be directly deduced from the specification of programP. |
| |
| Keywords: | fault-tolerant system temporal logic language XYZ/E refinement fault-tolerant transformation specification verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
