%0 Journal Article
%T 基于xyz/e描述和验证容错系统
%A 郭亮？
%A 唐稚松？
%J 软件学报
%P 913-920
%D 2002
%X 研究使用xyz/e描述和验证容错系统.基于xyz/e中可执行程序p对应的状态转换系统对其错误环境f建模,通过错误转换给出错误影响程序pf;基于p,f和恢复算法r,通过容错转换给出容错程序pf-r;定义了程序p,q之间两种求精关系:容错求精和向后恢复求精,基于这两种求精关系可直接从程序p的规范推导出程序q满足的一些性质.
%K 容错系统
%K 时序逻辑语言xyz/e
%K 求精
%K 容错转换
%K 规范
%K 验证
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20020506&flag=1