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

定理证明是一种形式化验证技术，也是形式化方法的重要组成部分，它能从形式规格说明中推理出应具备的性质与属性，从而可以对规格说明进行形式验证。Obiect-Z是形式规格说明语言Z的面向对象扩充，基于集合论与数理逻辑，具有严密的逻辑性，适合精确地描述大型软件系统，并且可以对其形式规格说明进行推理。本文首先给出了基于Object—Z规格说明的定理证明验证方法，接着用Object-Z描述了一个电梯操作系统的实例，在此基础上给出了其形式规格说明的定理证明方法来进行形式化验证。

Formal Verification Based on Object-Z Specification

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.