主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
郭亮,唐稚松.基于XYZ/E描述和验证容错系统.软件学报,2002,13(5):913-920
基于XYZ/E描述和验证容错系统
To Specify and Verify Fault-Tolerant Systems in XYZ/E
投稿时间:2000-07-20  修订日期:2001-07-06
DOI:
中文关键词:  容错系统  时序逻辑语言XYZ/E  求精  容错转换  规范  验证
英文关键词:fault-tolerant system  temporal logic language XYZ/E  refinement  fault-tolerant transformation  specification  verification
基金项目:国家863高科技发展计划资助项目(863-306-ZT02-04-01);国家"九五"重点科技攻关项目(98-780-01-07-01)
作者单位
郭亮 中国科学院,软件研究所,计算机科学重点实验室,北京,100080 
唐稚松 中国科学院,软件研究所,计算机科学重点实验室,北京,100080 
摘要点击次数: 2351
全文下载次数: 2795
中文摘要:
      研究使用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 realtionships,some properties satisfied by program Q can be directly deduced from the specification of programP.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利