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

Extending Slices of Object-Z Classes Based on Temporal Logic

作　　者：佟长英[1] 沈云付[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072

出　　处：《计算机技术与发展》2009年第6期13-16,21,共5页Computer Technology and Development

基　　金：国家863项目(2007AA01Z144)

摘　　要：文中对程序切片进行了研究,报告了程序切片的现状,进行了Object-Z类切片方面的调查。为使Object-Z规格易于验证,对Object-Z作切片处理是必须的。以Object-Z的通用堆栈类为实例,对类的描述进行扩展,给出了相应的Kripke结构。通过面向对象程序依赖图对Object-Z进行切片,实现了Object-Z的抽象,给出了对于一个类或具有继承关系的多个类的刻划,即证明了在状态和事件上的公式在原模型与抽象模型中保持,扩展了Object-Z类切片方法。In this paper, program slicing is studied and present situation of program slicing is reported, then Object - Z class slicing is investigated. In order to verify Object - Z easily, slicing is must be done. The description of class is extended and the corresponding Kripke structure is presented by taking general stack of Object - E as a case. Then the Object - Z is sliced by object - oriented program dependence graph and the abstraction of Object - Z is realized. A result about system properties by one class or many classes with inherited relations is proved. It is proved that formula on states and events preserves under origin model and abstract model. Finally, the slicing way of Object - Z class is extended.

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]