基于时序逻辑的Object-Z类切片的扩展

摘要：

文中对程序切片进行了研究,报告了程序切片的现状,进行了Object-Z类切片方面的调查.为使(Object-Z规格易于验证,对Obiect-Z作切片处理是必须的.以Ogject-Z的通用堆栈类为实例,对类的描述进行扩展,给出了相应的Kripke结构.通过面向对象程序依赖图对Object-Z进行切片,实现了Object-Z的抽象,给出了对于一个类或具有继承关系的多个类的刻划,即证明了在状态和事件上的公式在原模型与抽象模型中保持,扩展了Object-Z类切片方法.

关键词：程序切片、Kripke结构、Object-Z、时序逻辑、间隔逻辑、通用堆栈

所属期刊栏目：19

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家863项目2007AA012144

在线出版日期：2009-06-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：13-16,21