论文部分内容阅读
研究使用XYZ／E描述和验证容错系统。基于XYZ／E中可执行程序P对应的状态转换系统对其错误环境F建模，通过错误转换给出错误影响程序PF；基于P，F和恢复算法R，通过容错转换给出容错程序PF－R；定义了程序P，Q之间两种求精关系：容错求精和向后恢复求精，基于这两种求精关系可直接从程序P的规范推导出程序Q满足的一些性质。