基于xyz/e描述和验证容错系统
, PP. 913-920
Keywords: 容错系统,时序逻辑语言xyz/e,求精,容错转换,规范,验证
Abstract:
研究使用xyz/e描述和验证容错系统.基于xyz/e中可执行程序p对应的状态转换系统对其错误环境f建模,通过错误转换给出错误影响程序pf;基于p,f和恢复算法r,通过容错转换给出容错程序pf-r;定义了程序p,q之间两种求精关系:容错求精和向后恢复求精,基于这两种求精关系可直接从程序p的规范推导出程序q满足的一些性质.
Full-Text
