面向对象软件的形式验证技术

摘要

随着信息技术的发展，软件规模和复杂程度的日益增大，如何保证和提高软件质量成为软件界最为关心的问题之一。保证各种软件的正确性和提高软件的可靠性一直是人们研究的重点。20世纪60年代出现的“软件危机”表明软件项目中40％至60％的问题都是在需求阶段产生的，此过程中产生的问题包括收集、编辑、协商、修改产品需求过程中的手续和方法失误，非正式信息的收集，未确定的或不明确的功能，未发现或未经交流的假设，不完善的需求文档，以及突发的需求变更等。因此，在开发可靠的软件系统时，有效的规格说明技术，确认和验证手段是必需的。 人们研究形式方法希望帮助发现其它方法不容易发现的系统描述不一致性或不明确性，有助于增加软件开发人员对系统的理解，其目标是开发可靠的软件产品。形式方法的主要研究内容包括：形式规格说明(formal specification)和形式验证(formal verification)。定理证明(theorem proving)是一种形式验证方法，它是根据已构造的规格说明生成反映该规格说明应具有的性质，将其表示成定理形式，并加以证明，从而达到对系统规格说明验证的目的。 形式规格说明语言Obiect-z是形式规格说明语言z的面向对象扩充，基于数理逻辑与集合论，可以精确地描述大型面向对象软件，并且可以对它进行形式推理，以保证其正确性和一致性。Object-Z一般被用来描述一般的面向对象形式规格说明，但对于具有特定性质如行为子类型继承的规格说明，Object-Z难以描述。在Obiect-Z中，继承一般不保持行为子类型，本文提出了一种基于Object-z行为子类型继承来描述面向对象形式规格说明的方法。行为子类型是一种强子类型继承，具有很好的特征，原先验证过的规格说明适用于替代后的规格说明，不必再重新验证，为了增强对复杂系统的推理能力，可以直接使用这些已知的信息，既体现了规格说明重用又体现了验证重用。 安全关键系统(safety-critical system)经常有功能需求与时间要求，对于许多系统来说，实时系统的精确需求是必需的，而Object-Z不能描述面向对象实时软件系统。本文提出了两个扩充Object-Z的实时方法：功能部分与实时部分分离方法和用带时钟变量的线性时态逻辑扩充方法，扩充以后可以方便地描述与验证面向对象实时软件系统。 多态性是面向对象程序设计的一个重要特征，它允许使用一个子类对象来代替其超类的对象，应用到超类对象的操作会自动调用定义在子类中同名的操作。本文提出了一种关于多态性的推理方法，并实现推理的重用。一个形式规格说明是有用的，那它应该是一致的或非冲突的，本文研究了对形式规格说明的性质验证的方法，讨论了如何抽取满足相关性质的待证定理，即产生验证形式规格说明是否一致的，是否具有所需性质的证明责任(ProofObligation)。如果一个证明责任能够被证明，则说明此证明责任所相关的规格说明部分是一致的。 设计和开发验证工具对于提高验证效率，改善软件开发过程，保证软件质量具有重要意义，本文设计了一个Obiect-Z规格说明的证明责任产生器，可以产生相关的证明责任，这些证明责任可以输入到定理证明器Z/EVES中去证明之：先以Object-Z规格说明文件作为证明责任产生器的输入，接着按Z/EVES定理格式抽取证明责任，再把它作为Z/EVES定理证明器的输入文件。其中，所有的保存文件都是使用LATEX格式。

目录

文摘

英文文摘

声明

第一章前言

1.1软件需求

1.2需求规格说明

1.3形式方法

1.4形式规格说明

1.5形式验证

1.6定理证明技术

1.7论文的主要研究内容

第二章形式规格说明语言Object-Z

2.1语法

2.2语义

2.3形式验证方法

2.2.1初始状态存在性验证

2.2.2推理类中的性质

2.4实例研究：电梯操作系统

2.4.1描述

2.4.2形式验证

2.5小结

第三章产生证明责任验证Object-Z规格说明

3.1产生证明责任

3.1.1证明责任

3.1.2从基类中产生证明责任

3.1.3检查函数与操作符

3.1.4在继承下产生证明责任

3.1.5对象作为一个属性

3.1.6对相关的性质产生证明责任

3.2用Z/EVES验证证明责任

3.2.1证明器Z/EVES

3.2.2编辑

3.2.3分析

3.2.4验证

3.3小结

第四章Object-Z的多态性推理

4.1 Object-Z多态性

4.2多态性推理规则

4.3推理的重用

4.4实例研究

4.5小结

第五章行为子类型验证方法

5.1行为子类型定义

5.2实现Object-Z行为子类型继承

5.2.1不变式规则

5.2.2操作规则

5.3实例研究

5.4验证行为子类型规格说明

5.4.1对于不变式规则

5.4.2对于操作规则

5.4.3使用Z/EVES证明

5.5小结

第六章基于Object-Z的实时验证方法

6.1实时部分与功能部分分离方法

6.1.1时间变量定义

6.1.2语法

6.1.3操作完成的时间

6.1.4实例研究

6.1.5形式验证

6.2用带时钟变量的时态逻辑来扩充Object-Z

6.2.1 LTLC语法

6.2.2 LTLC语义

6.2.3 扩充 Object-Z的语法

6.2.4 扩充 Object-Z的语义

6.2.5完成的时间

6.2.6实例研究

6.2.7形式验证

6.3小结

第七章证明责任产生器的实现

7.1验证系统的结构

7.2验证系统的实现

7.2.1 Object-Z编辑器

7.2.2证明责任产生器

7.2.3两个实例

7.3小结

第八章结论与展望

8.1本文主要的工作

8.2将来的工作

参考文献

作者在攻读博士学位期间公开发表的论文及所参与的项目

致谢

附录