基于Object-Z的形式化验证方法  

Formal Verification Based on Object-Z Specification

作　　者：文志诚[1] 缪淮扣[1] 张新林[1] 

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

出　　处：《计算机科学》2007年第5期247-251,共5页Computer Science

基　　金：国家自然科学基金(60373072);上海市教委第四期重点学科建设基金资助

摘　　要：定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Object-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,适合精确地描述大型软件系统,并且可以对其形式规格说明进行推理。本文首先给出了基于Object-Z规格说明的定理证明验证方法,接着用Object-Z描述了一个电梯操作系统的实例,在此基础上给出了其形式规格说明的定理证明方法来进行形式化验证。Theorem proof, an important compositive part of formal method, is one kind of formal verification, which can reason about the characters that the formal specification Should hold for formal specification. Therefore, it can verify the formal specification. Object-Z, an extension to formal specification language Z, is apt to describing large scale object-oriented software specification and can reason about the formal specification. This paper presents a verification approach with theorem proof for Object-Z specification and describes an example of elevator operation system, whose relevant verification methods are given.

关 键 词：OBJECT-Z 形式化验证 前后置条件 状态空间 电梯操作系统 

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