（计算机软件与理论专业论文）基于形式规格说明的嵌入式定理证明技术的研究.pdf

上海大学硕士学位论文 摘要 如何提高软件系统的正确性是目前学术界和工业界均予以关注的重要研究 课题，研究人员提出多种解决方法，其中形式化方法被认为是解决问题的最有 希望的方法之一。 形式化方法是一种建立在严格数学基础上的软件开发方法。在软件开发过 程中使用形式化方法，可以提高目标软件系统的正确性和可靠性。但是，一般 来说，形式规格说明语言是不可执行的，而且，形式化方法是以严格的数学理 论为基础，用它来描述的软件需求规格说明比较抽象，用户难以确定规格说明 是否与他们的需求相一致。此外，形式规格说明是否具有用户所希望的性质也 需要进行验证。为此，人们提出要对形式化的需求规格说明进行确认和验证。 本文主要研究了软件需求规格说明的一种验证方法定理证明技术，研究 开发p v s z 定理证明原型系统。该系统能够对z 规格说明的定理进行证明，从而 实现对规格说明的验证。 p v s z 原型系统是通过将z 语义地嵌入到通用定理证明工具p v s 系统中实现 的。 首先，在p v s 系统中定义z 的类型和运算操作符，并且形式地推导了z 的基 本定律，用户可以在以后的证明过程中使用这些z 定律而无需知道它的语义，从 而建立了z 的工具库。 其次，在应用研究部分，我们根据z 规格说明语言的语法语义，制定了一系 列由z 规格说明到p v s 规格说明的转换规则。通过转换，可将z 的规格说明以 p v s 的理论形式表示出来，为定理证明做准备工作。 最后利用p v s z 定理证明原型系统，对规格说明的定理进行证明。通过具体 实例验证本系统能够有效地证明z 规格说明的相关定理，实现了对规格说明的性 质的验证。 关键词：形式方法，z 规格说明，定理证明，p v s v 上海大学硕士学位论文 a b s t r a c t n o w a d a y s ，h o wt oi m p r o v et h ec o n e c t n e s so fs o f t w a r es p e c i f i c a t i o nh a s b e c o m ea l li m p o r t a n tp r o b l e mw i t h i nt h ef i e l do f s o f t w a r ee n g i n e e r i n ga n di n d u s t r i a l r e s e a r c h e r sh a v ep r o p o s e dm a n ys o l u t i o n s ，a n df o r m a lm e t h o d sa l er e g a r d e df i t st h e m o s tp r o m i s i n gt e c h n i q u e st os o l v et h i sp r o b l e m f o r m a lm e t h o d sa r ek i n d so fs o f t w a r ed e v e l o p m e n tm e t h o d sb a s e do nr e g r o u s m a t h e m a t i c s i tc a ni m p r o v ec o r l e c t n c s sa n dr e l i a b i l i t yo fs o f t w a r es y s t e ma n dt h e e f f i c i e n c yo f s o f t w a r ed e v e l o p m e n t b u ti ng e n e r a l ，f o r m a ls p e c i f i c a t i o nl a n g u a g e sa r e a l m o s tn o n - e x e c u t a b l e m o r e o v e r , b e c a u s ef o r m a lm e t h o d sa r eb a s e do nt h et h e o r yo f m a t h e m a t i c s ，t h o s er e q u i r e m e n t ss p e c i f i c a t i o n sd e s c r i b e db yf o r m a lm e t h o d sa r ev e r y a b s t r a c ta n dd i f f i c u l tt ou n d e r s t a n d u s e r sc a l l tv e r i f yt h ec o n s i s t e n c yb e t w e e nt l l e i r i n f o r m a lr e q u i r e m e n t sa n df o r m a ls p e c i f i c a t i o n s o ，v a l i d a t i o na n dv e r i f i c a t i o no f f o r m a ls p e c i f i c a t i o nh a v e b e e ni n t r o d u c e d i nt h i st h e s i s ，w ed i s c u s so n eo f t h ev a l i f i c a t i o nm e t h o d so f f o r m a ls p e c i f i c a t i o n t h e o r e mp r o v i n g , a n dd e v e l o pat h e o r e mp r o v i n gp r o t o t y p es y s t e mn a m e dp v s - z w h i c hc a n p r o v et h et h e o r e m so f zs p e c i f i c a t i o na n dt h e ni m p l e m e n tt h ev e r i f i c a t i o n o f c o n s i s t e n c y t h i sp r o t o t y p es y s t e mi si m p l e m e n t e db ye n c o d i n gt h es e m a n t i co fzw i t h i na g e n e r a l p u r p o s et h e o r e mp r o v e rs y s t e mc a l l e dp v s f i r s t ，w ed e f i n et h eb a s i ct y p e sa n do p e r a t o r so fzl a n g u a g e ，a n df o r m a l l y d e r i v e dt h eb a s i czl a w st h a tc a l lt h e nb eu s e dw i t h o u ta n yk n o w l e d g eo f t h es e m a n t i c e n c o d i n g a f t e rt h a t , az t o o l k i ti si n s t a l l e d s e c o n d ，i nt h ep r o c e s so fa p p l i c a t i o nr e s e a r c h ，a c c o r d i n gt ot h es e m a n t i co fz s p e c i f i c a t i o n ，w ed e f i n e dt h et r a n s l a t i o nr u l e st h a tt r a n s l a t ezs p e c i f i c a t i o nt op v s s p e c i f i c a t i o n a f t e rt r a n s l a t i n g , w ec a ne x p r e s s et h ezs p e c i f i c a t i o nb yt h et h e o r yo f p v s a l lt h e s ea r e p r e p a r e df o rt h ew o r ko f t h e o r e mp r o v i n g f i n a l l y , w eu s ep v s - zs y s t e mt op r o v et h et h e o r e mo fzs p e c i f i c a t i o n ，a n d i n t r o d u c es e v e r a le x a m p l e s t h ee x p e r i m e n tr e s u l t ss h o wt h a ti tc o u l di m p l e m e n tt h e t h e o r e mp r o v i n go fs p e c i f i c a t i o n se f f e c t i v e l y , a n ds a t i s f i e dt h ea i mo fv e r i f y i n gt h e p r o p e r i t i e so f s p e c i f i c a t i o n k e y w o r d s ：f o r m a lm e t h o d s ，zs p e c i f i c a t i o n ，t h e o r e mp r o v i n g ，p v s v l 上海大学硕士学位论文 原创性声明 本人声明：所呈交的论文是本人在导师指导下进行的研究工作。 除了文中特另t j j j n 以标注和致谢的地方外，论文中不包含其他人已发 表或撰写过的研究成果。参与同一工作的其他同志对本研究所做的 任何贡献均已在论文中作了明确的说明并表示了谢意。 签名：叠望垄日期：主盟! a ：! 垒 本论文使用授权说明 本人完全了解上海大学有关保留、使用学位论文的规定，即： 学校有权保留论文及送交论文复印件，允许论文被查阅和借阅；学 校可以公布论文的全部或部分内容。 ( 保密的论文在解密后应遵守此规定) 签名：j 她导师签名：5 鸳筮睦日期：业 i i 上海大学硕士学位论文 第一章绪论 需求工程是随着计算机科学与技术及其应用领域的发展而发展的。在计算机 发展的初期，软件规模不大，软件开发所关注的是代码编写，需求分析很少受到 重视。后来软件开发引入了生命周期的概念，需求分析成为软件开发生命期中的 至关重要的阶段。随着软件系统规模的扩大，需求分析与定义在整个软件开发与 维护过程中越来越重要，直接关系到软件的成功与否。8 0 年代中期，形成了软 件工程的一个领域需求工程( r e q u i r e m e n te n g i n e e r i n g ，r e ) 。 本章将介绍课题的研究背景、意义，以及国内外的相关研究状况。 1 1 课题的研究背景 1 1 1 需求工程、软件需求规格说明 需求工程【l 】是应用已证实有效的技术和方法进行需求分析、确定客户需求、 帮助分析人员理解问题并定义目标系统的所有外部特征。它通过合适的工具和 记号系统地描述待开发的系统及其行为特征和相关约束，最后形成需求文档， 并对用户不断变化的需求演化给予支持。 需求工程可以分为系统需求工程( 针对由软硬件共同组成的整个系统) 和软 件需求工程( 仅针对软件部分) 。软件需求工程是一个不断反复的需求定义、文 档记录、需求演化的过程，并最终在验证的基础上冻结需求。 软件需求工程的主要结果是软件需求规格说明1 2 ( s o f t w a r er e q u i r e m e n t s p e c i f i c a t i o n ，s r s ) 。s r s 是对外部行为和系统环境( 软件、硬件、通信端口和 人) 接口的简洁完整的描述性文档。项目管理者用它来对项目进行计划和管理， 在许多情况下，它也被作为是用户的使用手册或帮助用户理解系统的文档。它广 泛地适用于对各类应用领域中的客户问题进行理解与描述，实现用户、分析员和 设计人员之间的通信，为软件设计提供基础，并支持系统的需求验证和演进。 s r s 的基本内容包括行为需求和非行为需求。行为需求定义系统需要“做什 么”，描述系统输入输出的映射及其关联信息，完整地刻画系统功能，是整个软 件需求的核心。非行为需求定义系统的属性，描述和行为无关的目标系统特性， 包括系统的性能、有效性、可靠性、安全性、易维护性、可见性和顺应性。 好的s r s 应具有如下特点：正确性、无二义性、完整性、一致性、可验证性、 上海大学硕士学位论文 可修改性、可跟踪性、易理解性以及有好的注解等。 1 1 2 非形式化方法、半形式化方法和形式化方法 现有的需求规格说明描述方法有三种：非形式化方法、半形式化方法和形式 化方法。表卜1 是三种方法的比较： 表1 1 非形式化方法、半形式化方法和形式化方法的比较 非形式化方法半形式化方法形式化方法 语法直观形式化形式化 语义直观直观形式化 歧义性最容易产生歧义有歧义歧义性较弱 可理解性最容易理解可以理解难以理解 精确性精确性最低 较为精确最精确 通过比较，可以看出： 非形式化方法使用未作任何限制的自然语言，易于理解和使用。但它具有固 有的二义性，且难以保证其正确性、可维护性，难以用计算机系统提供自动化的 支持。 半形式化方法介于非形式化方法与形式化方法之间，在宏观上对语言和语 义有较精确的描述，而在某些局部方面则允许使用非形式化的自然语言。 形式化方法是具有严格数学基础的描述系统特征的方法。( e n c y c l o p e d i ao f s o f t w a r ee n g i n e e r i n g ) ) 中对形式化方法的定义如下： 用于开发计算机系统的形式化方法是基于数学的用于描述系统性质的技 术。这样的形式化方法提供了一个框架，人们可以在该框架中以系统的而不是 特别的方式刻画、开发和验证系统 一个方法是形式化的，如果它有良好的数学基础，典型地，由形式化规格说 明语言给出。这个基础提供一种工具，可用精确的符号定义一致性和完整性，以 及更进一步，定义规格说明、实现和正确性。 由此可见，形式化方法具有准确、无二义性的特点，有助于验证有效性和完 整性。 形式化方法【3 的主要研究内容包括形式化的需求规格说明和形式化验证。形 式化规格说明是使用具有精确语义的形式语言对系统“做什么”的数学描述，它 是设计和编制程序的出发点，也是验证程序是否正确的依据。形式化验证包括规 格说明验证和程序验证。本文主要研究的是形式化规格说明的验证。 2 上海大学硕士学位论文 1 1 3 形式规格说明语言 形式化方法一般需要形式规格说明语言【4 】( f o r m a ls p e c i f i c a t i o n l a n g u a g e ) 的支持。 形式规格说明语言提供了一个称为语法域的记号系统和一个称为语义域的 目标集合，以及一组精确地定义了哪些目标系统满足哪个规格说明的规则。 使用形式规格说明语言来描述软件的需求规格说明，具有以下的优点： ( 1 ) 形式化规格说明以严格的数学概念和理论为基础，因而避免了使用自然 语言描述时可能带来的模糊性和歧义性。 ( 2 ) 形式化规格说明语言具有很强的抽象性，避免了在需求分析阶段对数据 结构和算法细节的详细描述； ( 3 ) 形式化规格说明可以通过自动化工具( 如定理证明器、模型测试器和动 画模拟等) 进行确认、验证以及求精变换，从而揭示或消除规格说明中的不一致 性、不完整性、重复性以及不明确性，增强对用户需求的洞察和理解，鼓励软件 可靠性、生产力和质量的改进； ( 4 ) 形式化规格说明确切地指出了目标系统各方面的特性，有助于系统的实 现。 当前已有许多形式规格说明语言被广泛使用，c p s 、l a r c h 、v d m 2 3 斟l 和z 是 充分展示上述特征的代表性形式规格说明语言。在本课题中，以z 规格说明语 言作为研究对象。 1 1 4 问题的提出 虽然使用形式化规格说明语言所描述的软件需求规格说明简洁而又紧凑，但 是同时它也比较抽象难懂。一般来说，形式化规格说明语言都是不可执行的，用 户和领域专家对形式规格说明和符号方面的知识了解甚少，很难理解形式规格说 明，也就难以确定规格说明是否与他们的需求相一致。为了清除形式规格说明中 的不一致性和模糊性，并确保能从规格说明中推断出所需的系统特征，我们必须 对形式规格说明进行确认( v a l i d a t i o n ) 和验证( v e r i f i c a t i o n ) 1 2 8 1 。 所谓确认就是对“软件满足用户需求”的描述进行一致性和完整性论证， 即“我们是否建立了一个正确的系统”。而验证则是对系统开发的每个阶段的输 出和前一个阶段的输出进行分析和推理，从而确保新阶段的输出满足了其前一 阶段输出所提出的需求，也就是“我们是否正确地建立了一个系统”。本文所要 研究的规格说明的定理证明技术( t h e o r e mp r o v i n g ) 就是一种验证方法。 上海大学硕士学位论文 1 2 研究形式规格说明的嵌入式定理证明技术的意义 尽管软件形式化方法有着这许多优点，可以满足工业上的许多需要，比如 说在早期发现缺陷，自动检查可能具有的性质，减少重复劳动，从而提高了软 件的质量。但是，多年来形式化方法并没有得到很广泛的应用。原因是多方面 的，比如说形式规格说明难以阅读，所以要对相关人员进行额外的训练：形式 方法并不能对客观世界的所有方面进行模型化；形式规格说明的正确性证明费 时费力等等，缺少有力的支持工具也是一个主要原因。现有的工具，例如定理 证明工具，模型检查工具是可用的，但是不能完全提供对z 规格说明的支持， 我们的工作是将一些方法和工具进行集成。 基于形式规格说明的定理证明有两种实现方法：一种是将规格说明语言集 成到一个成熟的定理证明工具中；另一种是专门构造一个针对该规格说明语言 的定理证明工具。后一种方法的实现有非常大的难度，完成这样的工作要耗费 大量的时间和人力。事实上，我们可以把现有的通用定理证明器与形式规格说 明语言集成，来取代一个专门的定理证明器。本课题是采用将z 规格说明集成 到定理证明器p v s ( p r o t o t y p ev e r i f i c a t i o ns y s t e m ，原型验证系统) 的方法来实现 对z 规格说明的定理的证明。 1 3 国内外研究现状 由于对z 规格说明语言缺少有力的证明工具，一些科研机构或个人对这一 问题进行研究。对z 规格说明进行定理证明的一种方法是先将z 规格说明嵌入 到已有的通用定理证明系统中，然后使用该证明系统对z 规格说明的性质进行 证明。目前，已有不少科研人员使用此方法进行了有益的尝试，也获得了一定 的成果。 b o w e n 和g o r d o n 曾在他们的论文 5 】中描述了将z 的语义嵌入到高阶逻辑系 统h o l 中，得到了z h o l 系统。该系统对z 给予了基本的支持，也通过了一 部分的实例测试，不过对z 的工具库的覆盖面还不够大，还不能应用于对大型 规格说明的实例的测试。 p r o o f p o w e r l 6 】是剑桥大学与程序验证公司等多家单位联合开发多年的商用 定理证明系统，它支持与h o l 系统同样版本的高阶逻辑，但是提供了不同的定 理证明基础。与h o l 相比，p r o o f p o w e r 的功能更为强大。相比之下，p r o o f p o w e r 系统是在z h o l 的基础上对z 的更深层次的嵌入。但是，p r o o f p o w e r 还不能够 对模式连接的证明提供有效的支持，并且在其逻辑中还缺少将z 语法映射到对 4 上海大学硕士学位论文 应的含义的语义函数。 另外，m a h a r a j 进行了zi nl e g o 系统的实现工作。在文中【7 】她详细地描述 了在l e g o 系统中如何表示z 语言中集合，函数，关系和数，但是对z 语言中的 其他数学结构如序列定义工作并未进行，并且只对z 数学工具库中的部分定律 进行了证明。在随后的工作中，她还研究了如何使用l e g o 定理检查器中实现的 依赖类型统一理论( u n i f y i n gt h e o r yo fd e p e n d e n tt y p e s ) 来对z 语言中的模 式进行编码，她的实现方法排除了将模式定义为类型的使用方法。由于相关类 型统一理论使用的是直觉逻辑，而z 使用的是经典逻辑，所以编码工作只覆盖 了z 的一部分。 在国内，还没看到有人在本领域的研究获得成果。 1 4 论文的主要研究内容 本论文是以作者攻读硕士学位期间承担课题的工作为基础，在第一章中阐 述了课题研究的来源、目的、意义以及国内外研究的现状。第二章介绍了z 规 格说明语言，包括z 语言的基本概念、基本结构，及其支持工具，阐述了z 规 格说明的验证方法，并着重介绍了其中的定理证明技术，包括实现的方法和实 现的难点。第三章介绍了p v s 系统，包括规格说明语言和定理证明器两大部分。 第四章给出了p v s z 系统的实现，以及规格说明的转换规则。第五章是利用 p v s z 原型系统进行了应用及实例研究，给出了实例说明。最后第六章总结全 文。 上海大学硬上学位论文 第二章z 规格说明的定理证明 形式化规格说明的定理证明是一种形式化验证方法，本章主要介绍z 规格说 明语言的基本概念、构造单元以及验证方法，并重点介绍了验证方法中的定理证 明技术及其实现方法。 2 1 z 语言的基本概念及其优点 z 语言 8 】是在1 9 7 9 年由j a b r i a l 和s s c h u m a n n 最早提出的，而后由h o a r e 所领导的英国牛津大学程序设计研究组p r g ( p r o g r a m m i n gr e s e a r c hg r o u p ) 进 行了大量的研究工作。 z 语言在早期发展阶段就己在政府、学校和工业部门得到了应用，成功的 例子有英国h u r s l e y 的i b m 公司应用z 对客户信息控制系统( c i c s ) 进行了规格 说明的重写，降低了软件开发费用，牛津大学的p r g 将z 应用于t r a n s p u t e r i n m o st 8 0 0 版本提供的浮点运算支持等。这些成功的应用对z 语言的发展产生 了较大的影响。在9 0 年代初，人们已经定义出了z 的标准文本。 2 i i 基本概念 z 语言是基于一阶谓词逻辑和集合论的形式规格说明语言，用于软件系统 功能的描述。称z 为形式语言是由于它采用了严格的数学理论。这样可以产生 简明、精确、无歧义且可证明的规格说明。同其它规格说明语言相比，z 一个 主要的特点是可以对z 规格说明进行推理和证明，这种特点使得软件开发人员 或用户能够很快找出规格说明的不一致、不完整之处，使他们提高对软件的信 心。 将z 语言称为规格说明语言的关键思想是把软件开发过程中的需求规格说 明阶段和设计阶段分开，在需求规格说明阶段精确地描述“做什么”，而不设计 “怎么做”。在z 的方法学中，我们强调的是“描述性”思维而尽量避免“过程 性”思维。规格说明阶段的目标是描述目标软件系统的功能，而不必过多地考 虑诸如效率和可实现性等问题。 2 i 2z 语言的优点 目前，z 也许是应用得比较广泛的形式化语言，尤其是在安全关键系统的 6 上海大学硕士学位论文 项目中z 语言的优势更加明显。z 语言之所以会获得如此多的成功，主要有以 下几个原因： ( 1 ) 可以比较容易地发现用z 写的规格说明的错误，特别是在自己审查规 格说明，及根据形式化的规格说明来审查设计与代码时，情况更是如此。 ( 2 ) 用z 写规格说明时，要求作者十分精确地使用z 的表示法。由于对精 确性的要求很高，从而和非形式化规格说明相比，减少了模糊性、不一致性和 遗漏。 ( 3 ) z 是一种形式化语言，开发者可以严格地验证规格说明的性质。 ( 4 ) 虽然完全学会z 语言有一定困难，但是，经验表明，只要学过离散数 学的软件开发人员可以只用比较短的时间就学会编写z 规格说明。 ( 5 ) 使用z 语言可以降低软件开发费用。虽然用z 写规格说明所需用的时 间比使用非形式化技术要多，但开发过程所需要的总时间却减少了。 2 2z 规格说明的构造单元 一个z 的文档是由形式的数学描述和非形式的解释所组成。形式的描述就 是形式规格说明，其基本构造单元是：基本类型定义、公理描述、模式和通用 式定义。 2 2 1 基本类型定义 在书写规格说明的一开始，首先要定义的是规格说明中要用到的基本类型。 这些基本类型有时被称为给定集合( g i v e ns e t s ) 。基本类型的定义就是一个类 型声明，它引入了一个或多个基本类型。例如： s t u d e n t ，b o o k 引入了基本类型s t u d e n t 和b o o k 。在引入了基本类型后，就可以使用这些类型 来声明变量。同一个规格说明中不同的基本类型没有相同的元素。例如，若x 被声明为类型s t u d e n t 的变量，则x 就不能成为类型b o o k 的变量。 基本类型是z 的类型系统的重要组成部分，对基本类型重复使用类型构造 符，可以构造其它的类型。 2 2 2 公理描述 公理描述引入了一个或多个全程变量和关于它们的谓词，这些谓词给出了 进一步的信息。一个公理描述具有如图2 1 所示的形式。谓词部分也可以不出 上海大学硕士学位论文 现。以操作系统中的存储块为例，系统中有n 个连续的编了号的存储块，用b 表示系统中所有自由存储块的集合，其公理描述如图2 2 所示： 图2 1 公理描述的形式图2 2 自由存储块b 的公理描述 在公理描述中，如果谓词部分不出现，则缺省的谓词就为t r u e ，可以用下面 的方式来引入一个全程变量： l m a x ：n 2 2 3 模式 z 语言最主要的结构是模式【9 】。模式是一个描述软件系统某一部分的数学 表示的正文，它含有声明部分和谓词部分。声明部分引入变量，并声明它们的 类型。谓词部分表示了关于变量的值的要求。模式可分为状态模式、初始状态 模式和操作模式。 ( 1 ) 状态模式 状态模式定义了目标软件系统某一部分的状态空间及其约束特性，系统中 该部分的状态存在于状态空间之中。如一个用来记录单位内部人员的生日名册 系统，可用图2 3 的模式来描述这个系统的状态。 n a m e ，d a t e 】 图2 3 生日名册的状态模式 模式上方为声明部分，n a m e 是人的集合，d a t e 是日期的集合，变量k n o w n 是已登记在册的姓名的集合，变量b i r t h d a y 是一个从n a m e 到d a t e 的函数。模 式下方为谓词部分，状态模式的谓词给出了状态不变式，它决定了这个系统的 约束是k n o w n = d o mb i r t h d a y ，即名册中的姓名集合与b i r t h d a y 的定义域相同。 上海大学硕士学位论文 ( 2 ) 初始状态模式 当用模式来描述一个系统的状态时，就必须对系统的初始状态进行描述。 一个系统的初始状态是系统建立时的状态。没有初始化的状态是很少的，也是 没有太大用处的。因此，初始状态模式也是z 规格说明的一个重要部分。对于 生日名册之例，其初始状态描述为模式i n i t b i r t h d a y b o o k ： 图2 4 生日名册的初始状态模式 初始化状态模式没有前状态，只有一个带有”修饰的后状态。该模式 赋予b i r t h d a y b o o k 的两个变量k n o w n 和b i r t h d a y 以明确的值。 初始状态模式的书写还往往牵涉到初始状态存在性的证明问题，即假设s 是状态模式名，系统的初始状态模式为i n i t s ，则初始状态存在性的证明问题 的形式为：卜| s e i n i t s 。 ( 3 ) 操作模式 操作模式定义了系统在状态空间上的操作。它描述了该操作所要满足的条 件以及前系统状态和操作后的系统状态之间的关系。如查询某人生日的操作模 式见图2 5 。 图2 5 查询生日的操作模式 在模式声明部分，巨b i r t h d a y b o o k 表明系统状态不发生改变。n a m e ? 为输 入变量，d a t e ! 为输出变量，谓词部分的前一个式子是表示输入变量的前置条件。 即进行一个操作时输入变量要满足的条件。后一个式子反映了输入、输出之间 的约束关系。关于z 语言的细节可参阅文献 4 。 9 上海大学硕士学位论文 2 2 4 通用式定义 在z 中，通用式结构有两种：一种是通用式定义，另一种是通用模式 ( g e n e r i cs c h e m a ) 。 通用式定义的一般形式如下图所示： 图2 6 通用式定义的一般形式 其中，嵌入在顶端双线中由一对方括号括起来的部分是通用式参数，声明 部分声明了通用式常量，谓词部分则是限制该常量的谓词。 通用模式定义的一般形式为： 图2 7 通用模式定义的一般形式 其中，s 是模式名，x ，是通用式形式参数，它可以作为类型在声明部分声明 变量时使用，声明部分和谓词部分与一般的模式定义一样。当要使用一个通用 式模式时，必须给通用式形式参数以具体值，例如：s s t u d e n t ，b o o k 2 3 z 规格说明的验证方法 一个软件项目是从用户需求的描述开始的，但这一需求描述是对软件的性 质的非形式化描述。在软件生命周期中，接下来就是分析需求描述，形成软件 需求规格说明，它是软件开发的重要参考文档，也是对软件产品进行确认和验 证的基础，这就要求软件需求规格说明的描述必须是清晰的、一致的和无二义 性的。 当前，许多软件工程的研究开始关注在软件需求规格说明和开发阶段应用 数学的方法。从2 0 世纪7 0 年代中期，研究人员提出了多种形式规格说明语言， 主要分为两类【lo ：一类是基于代数的语言，另一类是基于模型的语言，如z v d m 等。在软件工程中应用形式化方法的最主要原因是形式规格说明的精确性正是 软件系统的开发所需要的，并且它可以在软件开发阶段通过严密的验证来排除 1 0 上海大学硕士学位论文 错误。形式规格说明语言的良定义的语义和语法非常适合于对系统需求进行精 确的描述，并使得对规格说明进行形式化推理，以及对系统的设计和实现是否 符合需求进行证明成为可能。确切地说，数学的应用为软件开发引入了一门新 的方法学，我们称之为形式化软件开发方法学。在这种方法学中，软件产品的 开发阶段可分为以下步骤： ( 1 ) 使用形式规格说明技术描述软件产品的规格说明； ( 2 ) 对形式规格说明进行验证，确保其正确反映了用户的需求； ( 3 ) 对形式规格说明进行求精变换，产生高级语言的程序代码： ( 4 ) 对整个程序进行确认，以确保软件质量。 从上述步骤可以看出，一个有效的形式规格说明( 步骤( 2 ) ) 是非常重要的， 因为形式规格说明是后面的步骤( 步骤( 3 ) 和( 4 ) ) 的基础。 科研人员的不断研究和实践证明，对软件系统的设计和开发来说，形式规 格说明是十分必要的，尤其是对于一些大型的关乎安全的软件系统。目前，正 确性的验证问题也是学术界均予以关注的重要研究课题。我们可以从以下两个 事件切实感受到正确性验证的重要性。 1 9 9 6 年6 月4 日，欧洲航天局研制的阿里亚娜( a r i a n e ) 5 0 1 火箭在发射 升空3 7 秒后爆炸。事后调查发现，错误发生于当一个很大的6 4 位浮点数转换 为1 6 位带符号整数时出现异常。一个细小的错误，使得多年的努力毁于一旦。 2 0 0 0 年1 0 月，由于诺基亚提供的软件中的一个错误，造成德国一家移动电话 公司的通信服务被中断3 个多小时，这样的问题如果发生在战争环境下，后果将 是不堪设想。 从上述事件可以看出，软件是否可信赖已成为国家经济与国防等系统能否 正常运转的关键因素之一，尤其在一些高危险性领域更是如此。遗憾的是，软件 的设计与生产至今还缺乏坚实的科学基础和成熟的方法学，还没有令人信服的 办法能够论证或确认一个复杂软件系统是高度可靠安全的。如果说在复杂的软 件设计过程中出现错误是在所难免的，那么出现事故的唯一原因就是没有在产 品投入使用前对其进行完备的确认( v a l i d a t i o n ) 工作，即确认系统已经完全实 现了需求者的意图。 许多用户发现用z 表示方法建立规格说明来开发软件可以提高软件系统的可 靠性、正确性和效率。z 表示法的一个突出优点就是，能对它的规格说明进行形 式化验证。对于软件系统来说，尤其是那些安全性和可靠性要求很高的软件系统， 如果能产生一个对应于其形式规格说明可证明是正确的软件，那么将极大地提高 软件的质量。 对形式规格说明进行正确性验证有两种方法：模型检查和定理证明。 上海大学硕士学位论文 2 3 1 模型检查 模型检查【l l 】是一种针对有限状态并发系统的形式化自动验证技术，它通过 穷尽搜索系统的整个状态空间来检验该系统是否满足给定的性质。模型检查器 使用系统的一个有限状态模型，规格说明可表达为一个逻辑公式，模型检查器 对模型空间进行穷尽搜索，判断公式在该模型中是否满足。 模型检查方法的优点在于分析过程是完全自动进行的。当断定某性质不满 足时，模型检查能够提供反例，以便于定位设计错误。因此与推理相比，用户 无需掌握很复杂的数学技术。但是与定理证明器能处理十分抽象的空间相比， 模型检查器只能在系统被非常具体描述的情况下才能很好地工作。原因在于除 非模型检查器知道系统的整个空间，它才能进行搜索。 模型检查的主要缺点是状态爆炸问题【l 射，因为随着系统复杂程度的增加， 系统的状态数量将成指数级地增长，甚至一个简单的系统也会产生上百万个空 间。著名的例子包括应用s m v 来验证缓冲的一致性协议和用s p i n 来验证 a t & t 5 e s s 电话交换系统。可以说，模型检查技术的发展历史就是不断寻找新思 路、新策略和新算法来克服空间爆炸问题的历史。 目前，模型检查器主要用于硬件设计和协议的验证工作，由于它缺乏检查 软件规格说明性质所需的控制与数据结构，我们很难把目前的模型检查器完全 应用到软件规格说明的验证中。 2 3 2 定理证明 对规格说明进行验证的另一种技术是定理证明 ”2 酊。定理是可以从前提中 推导的正确的结论。定理证明技术可将系统和其期望的性质都表达为数学逻辑 中的公式。逻辑【2 明是由一个形式系统所规定的，逻辑定义了一组公理和推论规 则的集合。定理证明是用数学推理方法来证明一个实现是否满足了规格说明的 要求( 如图2 8 所示) 。形式规格说明可以通过证明某些性质是规格说明的逻辑 结果而得到验证。如果规格说明正确描述了需求，那它应逻辑上蕴含所有的正 确的结论。 i m p s p e ci 广1 11 i i l 一 l 。_ 一 e q u i v a l e n c e 。_ j 图2 8 定理证明 定理证明的优点是：高度的抽象性和强大的逻辑表示：可应用的范围较广。 1 2 上海大学硕士学位论文 同时，定理证明也有其局限性，目前，比较实用的定理证明的过程是交互性的， 需要人的引导。 定理证明系统由一组公理和规则组成，规则包括简化规则、重写规则、归 纳规则等。 定理证明系统一般可以分为自动定理证明系统和交互式定理证明系统。自 动定理证明系统的研究尽管有了很大的发展，特别是消解法的出现，为一阶谓 词系统的自动定理证明奠定了基础。自动定理证明系统的证明过程是完全自动 化的，但它只使用于一阶谓词系统，其典型代表是p r o l o g 系统【1 4 】。但是对于形 式化验证来说，比较实用的还是交互式定理证明系统。利用交互式定理证明系 统，人和机器可以一同工作，高层的证明由用户直接控制，而底层的证明由机 器自动处理，这样既发挥了人的创造性，指挥机器进行各种尝试，又发挥了机 器对琐碎事务的处理和记忆的特长。事实上，形式化验证的价值主要体现在验 证的过程中，设计者可以迸一步分析和理解设计，增强对设计正确性的信心， 并能够及时发现设计错误，而不是仅仅给出验证的结果，因此交互式定理证明 系统非常适合于形式化验证。 2 4z 规格说明的定理证明的难点 支持z 规格说明的证明并非一件容易的事情，其难点主要有两个方面： 2 4 1 语言表示法问题 z 规格说明是以传统的数学方法进行描述，这种表示法十分简洁扼要，用 户能够方便地使用z 书写规格说明和记录证明的过程，但是为了正确地处理z 规格说明，需要专门的字符处理和排版系统。而其他的规格说明表示法( 例如 在s p a r ka d a 中使用的表示法) 则是基于文本表示。另外，许多系统书写规格 说明使用的是一种语言表示法，而证明过程则采用另一种语言表示法。这样使 用起来更加复杂，并且增加了出错的可能性。 在规格说明和证明中使用何种语言表示法这个问题在软件工程领域是很重 要的。原因有两个方面： ( 1 ) 表示法的转换会增加理解的困难。尽管大多数用户能应付不同阶段所 使用的不同表示法，包括用于规格说明的输入，打印或排版，以及定理证明工 具交互操作，但是要熟练掌握这些表示法绝非易事，而且出错的几率会大大增 加。 上海大学硕士学位论文 ( 2 ) z 规格说明通常是完整开发过程的一部分，在每一个项目开发的过程 中，改动的情况时有发生，可能是需求方面的改动，也可能是发现了错误需要 进行改动，这就要求我们要对改动所带来的对需求规格说明文档、验证、精化 以及编码的一系列改动都要进行记录和跟踪。如果使用的工具，其输入表示法 各不相同，那么将很难对开发的过程进行有效的管理 由于z 的表示法问题会影响到证明的表达性和可读性，因此在开发z 的定 理证明工具时必须考虑这一问题。解决这一问题的方法是采用文本的方式来表 示z 规格说明，并与定理证明工具进行交互。 2 4 2 语义问题 在对z 规格说明进行推理的过程中，必须处理好以下两个问题： ( 1 ) 部分函数。 在书写z 规格说明过程中，通常会用到部分函数，因此，z 用户应确保在 使用部分函数时，函数作用在其定义域内。如果z 中对部分函数应用不在其定 义域内，则其结果取决于我们所使用的z 语义。用户常犯的一个错误是对一个 未知是否应用集合的势函数，如下例所示： 集合的势函数是一个部分函数，它的值仅在有穷集合上有定义。这样的定 义是否有意义取决于我们是如何处理