软件形式化方法第1章 绪论ppt课件.ppt

第章绪论,1.1 形式化方法概述1.2 软件开发中的形式化方法,什么是形式化方法？,“形式化”是相对“非形式化”或“半形式化”而言的一种分析问题、解决问题的思维方法。“形式化”是为了获得对问题(研究对象)的本质(逻辑的或数学的)认识，将问题(研究对象)从形形色色的具体背景中抽象出来，加以纯粹“符号化”以及严格“数学化”处理的思维方法和过程。,什么是形式化方法？,”形式化”可以定义为: 完全彻底的 抽象化+符号化+公理化 思维的过程,返 回,什么是形式化方法？,形式化方法是按照严格的数学逻辑规范对问题(研究对象)的本质进行形式化的抽象、定义、描述、建模、推理和验证等一整套理论和方法的总称。,形式化方法的起源,形式化方法的起源与现代逻辑学、语言学以及数学基础等领域的发展有着十分密切的关系。我们知道，逻辑上的严密性和表达上的简洁性，即避免出现所谓的逻辑悖论和不必要的冗余，是任何现代科学理论体系都不可或缺的生命力和价值所在。形式化方法的正是为了追求上述领域理论体系的严密性和简洁性而逐步发展起来的。随着现代科学技术的发展，形式化已成为许多学科领域，特别是数学和计算科学中最基本的研究方法和科学规范。,形式化方法的特征,研究手段：高度抽象表现形式：完全符号化表达方式：高度简洁内部过程：严格精确方法结果：普遍适用,高度的抽象性,抽象是任何一门科学乃至全部人类思维都具有的基本特性，然而，形式化方法的抽象程度远远超过自然科学中的一般抽象。其最大特点在于将现实事物从形形色色的具体背景中抽取出来，而仅仅以“纯符号化”的形式加以表现。,返 回,逻辑的严密性,形式化方法的高度抽象性和逻辑的严密性紧密相关。若没有逻辑的严密性，在自身理论中矛盾重重，漏洞百出，那么用形式化方法对问题(研究对象)进行抽象就失去了意义。正是由于形式化方法的逻辑严密性，我们在运用形式化方法解决问题时，只有严格遵守形式逻辑的基本法则，才能保证结论的正确性和可靠性。,返 回,结果的普遍适用性,形式化方法的高度抽象性和逻辑的严密性决定了其结果的普遍适用性。,返 回,形式化方法的作用,为系统开发提供精确简洁的形式化语言。为系统开发提供严格规范的形式化模型。为系统开发提供有效的逻辑推理工具。,返 回,形式化理论,形式化理论是由基本概念、基本原理或定律（联系这些概念的判断）以及由这些概念与原理逻辑推理出来的结论组成的体现，可以形式化地定义为： T=其中：T表示理论；C表示基本概念的集合；P表示基本原理或定律的集合；S表示由这些概念与原理逻辑推理出来的结论的集合。,公理化方法,公理化方法，是一种构造理论体系的演绎方法，它是从尽可能少的基本概念、公理出发，运用演绎推理规则，推出一系列的命题，从而建立整个理论体系的思想方法。,公理化方法,用公理化构建的理论体系称为公理系统，公理系统需要满足无矛盾性、独立性和完备性等3个条件：（1）无矛盾性：这是公理系统的基本要求，即不允许在一个公理系统中出现相互矛盾的命题，否则这个公理系统就没有价值。（2）独立性：公理系统中的所有的公理都必须是独立的，即任何一个公理都不能从其他公理推导出来。（3）完备性：公理系统必须是完备的，即从公理系统出发，能推出（或判定）该领域所有的命题。,公理化方法,为了保证公理系统的无矛盾性和独立性，一般要尽可能使公理系统简单化。简单化将使无矛盾性和独立性的证明成为可能。简单化也是科学研究追求的目标之一。,具体公理系统和抽象公理系统,在欧氏几何公理系统中，原始概念（点、线、面）和所有的公理都有直观的背景或客观的意义，像这样有现实世界背景的公理系统，一般被称为具体公理系统。由于非欧几何的出现，使人们感到具体公理系统过于受直觉的局限。因而，在19世纪末和20世纪初，一些数学家和逻辑学家开始了对抽象公理系统的研究。,具体公理系统和抽象公理系统,在抽象公理系统中，原始概念的直觉意义被抽象掉，甚至没有任何预先设定的意义，而公理也无需以任何实际意义为背景，它们无非是一些形式约定的符号串。这使得抽象公理系统可以有多种解释。,具体公理系统和抽象公理系统,例如，形式化的运算规则1+1可以解释为一个苹果加一个苹果，或者为一本书加一本书。布尔代数抽象公理系统可以解释为有关命题真值的命题代数，或者有关电路设计研究的开关代数。在这些解释中，抽象符号X可以分别被看作“命题X”、“电路X”等，“0”和“1”分别被用于表示命题的“假”和“真”，或者电路的“开”和“闭”。,在欧几里德的几何原本中，用公理化方法对当时的数学知识（平面几何）作了系统化、理论化的总结。他以点、线、面为原始概念，以5条公设和5条公理为原始命题，给出了平面几何中的119个定义，465条命题及其证明，构成了历史上第一个数学公理体系。,下一页,例：平面几何（欧氏几何）的公理化概括,原始概念：点、线、面原始命题（公设）：公设1：两点之间可作一条直线；公设2：一条有限直线可不断延长；公设3：以任意中心和直径可以画圆；公设4：凡直角都彼此相等；公设5：在平面上，过给定直线之外的一点，存在且仅存在一条平行线，即所谓的“平行公设（公理）,下一页,例：平面几何（欧氏几何）的公理化概括,原始命题（公理）：公理1：等于同量的量彼此相等公理2：等量加等量，和相等公理3：等量减等量，差相等公理4：彼此重合的图形全等公理5：整体大于部分,返 回,例：平面几何（欧氏几何）的公理化概括,公理化方法在计算学科中的应用,公理化方法主要用于计算学科理论形态方面的研究。在计算学科各分支领域，均采用了公理化方法，如:形式语义学关系数据库理论计算认知领域,形式化系统,任何按照形式化思想建立的具有“符号化”和“公理化”特征的抽象系统都可以称为形式化系统。,下一页,形式化系统,一个形式化系统一般由下面几个部分组成：初始符号：初始符号不具有任何意义。形式规则：形式规则规定一种程序，借以判定哪些符号串是本系统中的公式，哪些不是。公理：即在本系统的公式中，确定不加推导就可以断定的公式集。变形规则：变形规则亦称演绎规则或推导规则。变形规则规定，从已被断定的公式，如何得出新的被断定公式，被断定的公式又称为系统中的定理。,下一页,在以上4个组成部分中，前两个部分定义了一个形式语言，后两个部分在该形式语言上定义了一个演绎结构。形式化系统由形式语言和定义于其上的演绎结构组成。,返 回,形式化系统,从某种意义上讲，任何计算机系统软硬件都是一种形式化系统，它们的结构可以用形式化方法描述。程序设计语言也是一种形式语言系统。,返 回,形式化系统,抽象性抽象是人们认识客观世界的基本方法，虽然抽象性并不是形式化系统的专利，但形式化系统具有更强的抽象性。,返 回,形式化系统的基本特点,符号化形式化系统的抽象性表现在它自身仅仅是一个符号系统，除了表示符号间的关系（字符号串的变换）外，不表示任何别的意义。,返 回,形式化系统的基本特点,形式化系统的基本特点,严格性形式化系统中，任何初始符号和推导过程都要进行严格的定义。机械化形式化系统采用的是一种纯形式的机械方法，因此它的严格性高于一般的数学推导。,下一页,形式化方法的局限性,形式化方法并不是“完美无缺”的“灵丹妙药”。可以证明，任何一个形式化系统，如果它是无矛盾的，那么，它就具有下面两个局限性。,下一页,形式化方法的局限性,不完备性1931年，哥德尔提出的关于形式化系统的“不完备性定理”，指出：如果一个形式的数学理论是足够复杂的（复杂到所有的递归函数在其中都能够表示），而且它是无矛盾的，那么在这一理论中必存在一个语句，这一语句在这一理论中既不能证明，也不能否证。,下一页,31,哥德尔不完备定理,哥德尔不完备定理是库尔特哥德尔（Kurt Gdel 19061978）于1931年证明并发表的两条定理。第一定理：任何一个相容的数学形式化理论中，只要它强到足以蕴涵皮亚诺算术公理，就可以在其中构造在体系中既不能证明也不能否证的命题。第二定理：任何相容的形式体系不能用于证明它本身的相容性。,32,歌德尔不完全定理对认知科学哲学的影响,哥德尔不完备定理的结论影响了数学哲学以及形式化主义（使用形式符号描述原理）中的一些观点。我们可以将第一定理解释为：“我们永远不能发现一个万能的公理系统，能够证明一切数学真理，而不能证明任何谬误。”我们可以将第一定理解释为：“如果一个（强度足以证明基本算术公理的）公理系统可以用来证明它自身的相容性，那么它就是不相容的。”,不可判定性如果对一类语句C而言，存在一个算法AL，使得对C中的任一语句S而言，可以利用算法AL来判定其是否成立，则C称为可判定的，否则，称为不可判定的。著名的“停机问题”就是一个不可判定性的问题。该问题是指一个任给的图灵机对于一个任给的输入而言是否停机的问题，图灵证明了这类问题是不可判定的。计算机系统是一种形式化系统，因此，计算机系统一样也具有形式化系统的局限性。,返 回,形式化方法的局限性,形式化与公理化,形式化不一定导致公理化，公理系统也不一定是形式系统。如欧氏几何公理系统就不是形式系统。形式化与公理化虽然不同，但在近代数学中，形式系统大都是形式化的公理系统。,第章绪论,1.1 形式化方法概述1.2 软件开发中的形式化方法,计算机软件一般指计算机系统中的程序及文档程序:以计算机语言表达的软件系统文档:以人类语言(自然的或形式化的)表达的软件系统二者互相配合共同构成了完整的软件系统人类的经验、抽象知识正逐步由软件予以精确地体现,什么是软件？,万物皆数?,通过软件，人们可以对其所认识到的任何一种事物进行“编码”。以产生它的一个数字化的虚拟“实例”。,软件本质：逻辑产品,理论基础：Universal TM（图灵机）von Neumann architecturePL virtual machines,软件是人类脑力劳动的产物是系统逻辑的体现 但又必须依附于一定的载体例如：纸张、软盘、硬盘、光盘等 其它物品呢？需不需要载体？理解软件的关键是什么？,软件本质：逻辑产品,软件作为逻辑产品的特点：优势：易于变化，适应性强复制成本低，适合规模经济劣势：不易被理解容易出错找错、排错困难,软件本质：逻辑产品,41,软件开发过程,软件开发把现实世界的需求模型化成软件并予以实现的过程软件开发的主要步骤（大致，有不同说法）：问题和需求分析设计：功能设计结构设计编码（构建）调试发布、维护和升级,人们在实践中提出了许多开发模型：如传统的瀑布模型，较新近的有快速原型、迭代式开发模型等等,-42-,软件开发的历史,软件开发的三个阶段程序设计阶段（1946年-1956年）科学计算、机器语言及汇编语言、个体编程编程技巧、程序效率没有文档、软件一词尚未出现程序系统阶段（1956年-1968年）1956年，J.Backus Fortran语言诞生大量数据处理、小组开发“软件”一词出现：程序及其说明60年代中期，软件危机。软件工程阶段（1968年以来）1968年NATO会议，提出“软件工程”术语工程化方法、描述语言、团队开发,43,软件开发：实际情况,软件开发的实际情况并不乐观。项目经常延误，预算经常超支。开发的后续阶段常发现许多前期设计错误，更正的代价高昂。发布运行的软件中常常存在着许多错误，时常崩溃软件维护和更新工作的代价很高。,44,软件开发：实际情况,Therac-25 放射线治疗仪1985-87 年过量辐射 (6 个死亡 / 截肢)！,45,软件开发：实际情况,航空器控制系统功能错误 (飞机撞毁)！,46,软件的本质问题,复杂性规模：成万、成百万、甚至成千万行代码系统组成部分之间异常复杂的直接与间接相互作用静态结构与动态性质之间难以把握的复杂关系不确定性/多变性需求的不断提升和变化异常丰富多彩的应用需求困境要求较低的开发成本和较短的开发周期难以长期集中一大批最优秀的技术人员,An example of a real architecture in an industry,软件的复杂性,软件的不确定性,Heisenberg不确定性：由于软件的开发和使用，造成了由软件、使用者及其环境所构成的系统发生了变化，这样的变化是难以预测的，由此产生的不确定性Gdel不确定性：对一个软件，由于使用者及其环境所构成的系统的描述的不完备所造成的不确定性,应对方法,软件：设计和制造,传统的认识是软件没有制造过程，只有设计过程按照传统说法，软件的实现阶段也被称作“程序设计”在传统的软件开发过程中，前期各个阶段的工作成果都是自然语言描述的“非形式化”的文档，只有最后开发阶段的成果才是“形式化”的程序代码非形式的前期工作成果（文档）只能由人以非形式的方式阅读、理解和讨论，无法进行严格的分析的推理,软件：设计和制造,从原则上说，程序代码都是“形式化”的，有“严格”定义的语法和语义。程序的所有静态和动态性质都蕴藏在程序正文中，其特点是：程序除包含了软件的功能逻辑外，还包含了许多有关具体语言、实现模型的细节，使对程序逻辑详细分析变得非常困难。各种实现细节大大增加了程序的复杂度，从而大大提高了分析和推理的成本（通常不是规模的线性函数，而是指数的）。,软件：设计和制造,由非形式化的软件前期成果(文档)到后期的复杂烦琐的程序代码，这一跨越的距离太大，相互之间的关系难以把握，无法验证对错。由于，软件的严格的形式化描述出现在后期，形式太复杂，与前期成果的距离太远，导致对程序代码的分析和推理障碍重重，并且不完整。测试不可能完全，发现问题的能力很有限，不能成为评判标准。,53,软件：设计和制造,可以把软件的前期工作看成设计，把最后的编程看作制造为了提高软件质量，必须加强软件的设计过程，需要：更可控的设计和制造过程为设计本身提供更好的基础支持（理论和技术、工具）在设计过程的早期，能够严格地分析前期制品的内在性质，尽早发现并更正设计中隐藏的错误和缺陷清晰而无歧义的制品描述形式，在不同方面和不同细节程度的设计之间建立严格定义的、可以严格检查的关系从设计到制造的严格而清晰的转换，定义清楚什么是正确的实现，并能正确实施实际的制造活动在软件设计阶段引进严格的形式化描述，就可以对早期成果进行分析和推理，为实现（制造）打下更好的基础。,形式化方法的引入,从以上分析不难看出，在软件设计实现的各阶段(特别是早期)引进严格的形式化描述，对软件开发的早期成果进行分析和推理，将可以为后续开发打下更好的基础。在设计过程中采用严格的数学或逻辑方法分析前期制品的内在性质，将可以尽早发现并更正设计中隐藏的错误和缺陷。采用清晰而无歧义的描述形式，在设计和实现之间建立严格定义的关系（即什么是正确的实现），以便实现软件开发过程的自动化。,朴素方法、形式化方法和半形式化方法,非形式化方法的缺点,用自然语言书写系统规格说明书，可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。前期工作成果（文档）只能由人以非形式的方式阅读、理解和讨论，难以进行严格的分析和推理。前期工作成果到复杂程序代码的跨越距离太大，相互之间的关系难以把握，无法保证质量。,形式化方法的优点,能够简洁准确地描述物理现象、对象或动作的结果，是理想的建模工具。可以在不同的软件工程活动之间平滑地过渡。不仅功能规格说明，而且系统设计也可以用数学(代码)表达。提供了高层次的确认手段：可以使用数学方法证明：设计符合规格说明，程序代码正确地实现了设计结果。,软件形式化方法的定义,用于开发计算机系统的形式化方法是一种基于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框架，人们可以在该框架中以系统的方式刻画、开发和验证系统。 Encyclopedia of Software Engineering,软件形式化方法的定义,在软件开发的全过程中，凡是采用严格的数学语言，具有精确的数学语义的方法，都称为形式化方法。从广义角度，形式化方法是软件开发过程中分析、设计及实现的系统工程方法。,软件形式化方法的定义,狭义地，软件形式化方法又分为形式化规格（specification）方法和形式化验证（verification）方法。形式化规格是通过具有明确数学定义的文法和语义的方法或语言对软件的期望特性或者行为进行的精确、简洁描述。形式化验证是基于已建立的形式化规格，对软件的相关特性进行数学分析和证明。,软件形式化方法的目的,软件形式化方法的主要目的是保证软件的正确性。形式化方法基于严格的数学，而在软件开发过程中使用数学具有如下优点：数学是最准确的建模媒体，能够对现象、对象、动作等进行简洁、准确的描述；数学支持抽象，它使得规格的本质可以被展示出来，并且还可以以一种有组织的方式来表示系统规格中的抽象层次；数学提供了高层确认的手段，可以使用数学证明来揭示规格中的矛盾性和不完整性、以及用来展示设计和规格之间的一致情况等。,形式化规格说明的期望特性一致性、完整性及无歧义性是所有规格说明方法的目标。形式化方法的使用增加了这些理想实现的可能性。,软件形式化方法的目的,规格说明语言的形式化语法使得需求或设计以唯一的方式被解释，从而排除了读者解释自然语言(例如英语)或图形表示时经常产生的歧义性;集合论和逻辑符号的描述便利使得可以清晰地陈述事实(需求)；要达到一致，在规格说明中某地方陈述的事实就不能与其他地方有矛盾。一致性是通过数学证明将初始事实形式化地映射(使用推理规则)到规格说明中后面的陈述来保证的。,软件形式化方法的目的,软件形式化方法的过程,基于转换模型的软件开发过程实际上可理解为：从最高层的规格开始，通过一系列的求精变换步骤，每一步都降低一些抽象程度或增加一些可执行性，最终得到能够指导计算机明确执行的程序代码。在进行求精的过程中要保证转换之间的一致性和正确性，保证所得到的程序能够满足最初的规格。这种正确性和一致性可以通过求精过程中所遵循的一系列规则来保证，也可以在事后采用验证工具来证明。,65,形式化开发实例：销售管理,假设我们要开发一个商店的销售管理系统：客户管理，根据情况将客户分为三类：正常客户，优惠为0，默认一次信用卡消费限额为1000元VIP 客户，优惠10%，有较高的信用卡消费限额可疑客户，优惠为0，有较低的信用卡消费限额货单管理（POS 机端）库存管理,66,客户结构和性质,基本集合：,常量和属性：,变量和不变式：,67,客户相关操作,加入客户：,修改允许值：,68,形式化开发,这样写出的一组集合、常量、变量和相关操作的规范，构成了一个“抽象数据类型(ADT)”（在比程序更抽象的层次上的描述，B 方法中称为抽象机）一组这样的抽象机规范描述了一个软件系统,这样的描述与程序有什么不同吗？采用高层的概念（集合论、逻辑），没有具体的实现细节描述的是性质和关系，其中没有过程性可以验证各个操作是否满足不变式（从满足不变式的情况出发，经过任何一个操作，结果得到的状态是否仍然满足不变式）基于一种严格定义的规范语言，可以开发相关工具帮助我们验证相应规则中有没有问题（一个抽象机是否完全，是否自圆其说）可以通过严格定义的精化步骤，增添新的实现细节，或者用更接近实际程序设计语言的结构代换抽象结构，逐步做出最终的程序精化操作的正确性同样可以证明,69,形式化开发实例,形式化开发方法能用于实际吗？,下面介绍两个实际开发实例巴黎地铁14号线自动驾驶系统，1998投入运行巴黎Roissy机场自动穿梭车，2006年投入运行,70,形式化开发实例,两个系统中的关键部分（包括自动驾驶等）用 B 方法开发开发过程：根据软件需求文档构造系统的抽象模型由工具自动抽取需要证明的定理（不变式维持定理）不断扩充已有模型，重复2、3步，直至得到一个完整的抽象模型并证明了所有的不变式定理（需要一定人工参与）开发软件系统的更具体的模型，加入细节，使更多的操作具体化，用更接近计算机实现的数据结构代替更抽象的结构证明新的具体模型是更抽象的模型的“精化”。为此相应工具将自动生成一组“精化关系定理”，并证明这些定理（需要一定人工参与）通过不断重复第4、5步，最终做出一个可以直接对应到实现的模型用一个工具，从最终模型直接生成可执行的程序（Ada 语言程序）,71,形式化开发实例,一些情况：,正在采用类似的方式进行开发的系统：纽约城市地铁，巴塞罗那地铁，布拉格地铁，巴黎地铁1号线 等,有关材料取自：Jean-Raymond Abrial, 工业开发中的形式化方法：成就，问题和未来，2006 年国际软件工程大会（ICSE）特邀报告,软件形式化方法发展历史,形式化技术最早是从戴克斯特拉和霍尔（C.Hoare）在程序验证方面的工作和斯科特（D.S.Scott）以及其他学者在程序语义方面的工作发展起来的。,软件形式化方法发展历史,自20世纪60年代末以来，许多学者开展了软件形式化方法的相关研究，其源头包括：Dijkstra和Hoare在程序验证(或称程序正确性证明)方面的工作。Scoot和Stratchey等人在形式语义学方面的工作。目前，形式化技术已经成为计算机科学的一个重要分支和研究领域，其作用相当于传统工程技术（如计算流体动力学）在航空设计中的作用。,软件形式化方法发展历史,被最早应用的软件形式化方法是”逻辑与逻辑推理”，它的目标是使推理过程机械化，但是，这一目标受到许多挫折。其主要原因包括：逻辑系统的不完备性(incompleteness)、逻辑系统的不可判定性(undecidability)、自动推理的难处理性(intractability)。但是在一些实际应用上，逻辑方法和自动推理还是起着非常大的作用 。,软件形式化方法发展历史,早期形式化方法在软件验证的应用是串行程序的验证，后来随着软件研究和应用的发展，逐渐多样化。用逻辑和代数方法描述软件，用逻辑推理来验证软件的性质（即描述软件的逻辑公式）。用进程代数描述并发软件，用模型检测方法验证这些软件的性质。,形式化规范和形式化验证,软件形式化方法原则上是用数学与逻辑方法描述和验证软件系统。从总体上看，形式化方法可以分为“形式化规范”和“形式化验证”两个方面。,形式化规范,规范就是对系统或者对象及其期望的特性或者行为进行的描述。规范所要描述的内容包括：功能特性、行为特性、结构特性、时间特性。,下一页,形式化规范,功能特性侧重于系统的功能方面，即做什么。行为特性侧重于系统的具体行为演化，即如何做。结构特性侧重于系统的组成，各个组成部分或者子系统间的联系和复合。时间特性则是时间相关的系统特性。,下一页,形式化规范语言,形式化规范语言以严格的数学概念和理论为基础，具有明确的、无二义性的语法和语义。这些语言包括: 命题逻辑，一阶逻辑，高阶逻辑，代数，状态机，并发状态机，自动机，计算树逻辑，线性时序逻辑，进程代数， -演算， -演算，特殊的程序语言以及程序语言的子集等。,形式化规范的优点和缺点,优点：有严格的语义、语法定义。在形式化建模过程中，有查错和分析验证功能，能支持计算机检查出模型中矛盾的地方。可由计算机自动地把形式化规格说明变换到各种计算机系统环境上。所以最终在计算机上实现的软件，是从模型中把矛盾和暧昧之处都去掉的高质量软件。缺点：形式化模型和作为描述对象的现实世界很难直接对应，所以很难直接从现实世界获取形式化模型。,形式化规范的分类,形式规范按照描述系统的特性可以分为三类： 1) 描述顺序系统行为的形式规范方法典型有Z，B，VMD这类方法中状态使用集合，关系和函数等数学结构来表示;状态转移使用前置条件和后置条件来表示 2) 描述并发系统行为的形式规范方法典型有时CSP，CCS，序逻辑和I/O自动机这类方法中状态只使用简单的数学类型例如整数或对状态根本没有定义系统的行为用序列，树或事件的编序关系来表示 3) 集成的形式规范方法典型有SDL，RAISE它们把两种不同的方法结合起来，既能表示复杂的状态类型又能描述并发系统的特性,形式化验证,形式验证是指使用严格的数学方法来推理验证产品或设计是否符合其全部或部分规范的过程。形式验证要求产品的规范和实现均需要有严格的形式描述。,形式化验证,目前形式验证主要有两种方法：模型检验(Model Checking)定理证明(Theorem proving)两种方法都是使用形式方法来分析一个系统是否满足所期望的特性。,模型检验(Model Checking),模型检验是一种基于有限状态模型并检验该模型的期望特性的技术。粗略地讲，模型检验就是对模型的状态空间进行蛮力搜索，以确认该系统模型是否具有某些性质,搜索的可终止性依赖于模型的有限性。模型检验主要适用于有穷状态系统，其优点是完全自动化并且验证速度快。模型检验也可用于系统部分规格，即对于只给出了部分规格的系统，通过搜索可以提供关于已知部分正确性的有用信息。,模型检验(Model Checking),此外，当所检验的性质未被满足时，将终止搜索过程并给出反例，这种信息常常反映了系统设计中的细微失误，因而对于用户排错有极大的帮助。模型检验方法的一个严重缺陷是“状态爆炸问题”，即随着所要检验的系统的规模增大，模型检验算法所需的时间/空间开销往往呈指数增长，因而极大限制了其实际使用范围。,定理证明,定理证明就是从系统的公理出发使用推理规则逐步推导出其所期望的特性的过程。定理证明采用逻辑公式来规格系统及其性质，其中的逻辑由一个具有公理和推理规则的形式化系统给出，进行定理证明的过程就是应用这些公理或推理规则来证明系统具有某些性质。证明所需要的步骤依赖于系统的公理和推理规则，在某种程度上也依赖于其派生定义和中间引理。,定理证明,不同于模型检验，定理证明可以处理无限状态空间问题。定理证明系统又可以粗略地分为自动和交互式两种类型。自动定理证明系统是通用搜索过程，在解决各种组合问题中比较成功。交互式定理证明系统需要与用户进行交互，要求用户能提供验证中创造性最强部分（建立断言等）的工作，因而其效率较低，较难用于大系统的验证。,软件形式化方法的分类,根据对目标软件系统说明的方式，软件形式化方法可以分为： (1)面向模型的方法 (2)面向性质的方法,软件形式化方法的分类,根据表达方式，形式化方法又可分为：(1)基于模型的方法：给出系统的状态和状态变换的显式操作，但不给出并发的显式表示如：Z和VDM(2)基于代数的方法：通过联系不同操作之间的关系，来给出操作的隐式定义，但不定义状态，同样它也不给出并发的显式表示如：OBJ，LARCH，CLEAR(3)基于过程代数的方法：给出并发过程的一个显式模型，并通过过程间的通信约束来表示行为如：CSP、CCS,软件形式化方法的分类,(4)基于逻辑的方法：用逻辑来描述系统的特性，包括程序行为的低级规范和系统时间行为的规范如：时序逻辑法，实时区间逻辑法，直觉命题逻辑法，高阶逻辑法(5)基于网的方法：根据网中的数据流，显式地给出系统的并发模型，包括网中从一个结点流向另一个结点的条件。如：Petri网，谓词变换网等,软件形式化方法的分类,在实际应用中，往往将多种方法混合使用。使用时多以集合论和谓词逻辑为基础这些方法在技术上都有些相似，但在表达能力上却有不同。,软件开发中为什么使用形式化方法,（1）保证质量的需要（2）节约成本的需要,（1）保证质量的需要,为了得到高质量的软件，我们强烈希望使用软件工程中最好的实践经验和方法。软件缺陷往往会引起客户的恐慌甚至愤怒，而在更坏的情况下可能会给客户的业务造成较大的破坏或者造成生命损失。因此，企业要采用最好的实践，使他们的软件过程变得成熟起来。形式方法是一种前沿技术，研究表明，这种技术非常有助于那些希望把软件产品的缺陷出现率减到最小的企业。,（2）节约成本的需要,有证据显示，形式方法的使用减少了项目成本。例如，IBM的大型CICS事务处理项目的独立审核表明，9的成本节约要归功于形式方法的使用。对T800型变换计算机的Inmos浮点单元的独立审核也证明，形式方法的使用估计可以减少12个月的测试时间。,形式方法和复用,有效的软件复用(Reuse)有助于提高软件开发的生产率，这在应用软件的快速开发中具有特殊的意义。软件复用的思想是开发出可在未来项目中使用的基本部件，这就要求部件具有高质量和高可用性，而且部件的实际行为和使用环境也要具备一个文档化的描述。,形式化方法和常规方法的比较,形式化方法和工程界的常规方法相比最明显的区别在于它们的开发原则 不同。形式化方法希望尽可能直接构造出正确的系统。而常规方法认为错误不可避免，因此必须通过测试尽可能地发现系统中的错误并加以纠正。,形式化方法和常规方法的比较,开发原则不同决定了开发模式的差别。在使用形式化方法的开发过程中，需求分析和设计阶段投入很大工作量，需要的工作量通常占软件开发全部工作量的55%-65% ，而编码和测试阶段的工作量相对较小，只占全部工作量的35%-45%。,应用形式化方法的准则,选择适用于当前项目的符号系统。应该形式化，但不要过分形式化。通常没有必要对系统的每个方面都使用形式化方法。应该进行成本/效益分析。需要有形式化方法的顾问。不要放弃传统的开发方法。把形式化方法和结构化方法或面向对象方法集成起来是可能的，而且由于取长补短往往能获得很好的效果。,应该建立详尽的文档。建议使用自然语言注释来配合形式化的规格说明，以帮助读者理解系统。不应该放弃质量标准。在系统开发过程中必须一如既往地实施其他SQA活动。不应该盲目依赖形式化方法，这种方法并不能保证系统绝对正确。应该测试、测试再测试。由于形式化方法不能保证系统绝对正确，因此，软件测试的重要性并没有降低。应该重用。即使使用了形式化方法，软件重用仍然是降低软件成本和提高软件质量的唯一合理的方法。,应用形式化方法的准则,形式化方法和常规方法的比较,而常规的工程开发方法的编码和测试阶段所需的工作量非常大，要占到全部工作量的60%-70% 另外，许多项目只在部分阶段使用形式化方法，或者是把形式化方法和其它软件开发方法结合起来使用,形式化方法的实践,近年来，出现了许多采用形式化方法开发的软件系统实例，特别是在各种安全攸关和生命攸关系统开发中，使用形式化方法已成为强制性要求，例如：交通工具（汽车、飞机等）控制系统交通指挥调度系统自动化运输系统核电站控制系统,形式化方法的实践,形式化方法在硬件领域得到广泛应用，例如：90年代Intel 的奔腾芯片浮点运算器错误造成了很大的经济损失，使许多硬件公司从中汲取经验和教训。90年代Moore等人受AMD公司委托，证明了ABD K5浮点运算器的正确性，并为各种硬件厂商做了许多形式化验证工作。目前，模型检验技术在硬件领域得到广泛的应用，已经成为硬件设计中的标准常规技术。各大硬件公司都在设法招募形式化方法、模型检查等领域的专业人员（博士毕业生、博士后等），开展硬件的形式化分析和验证工作。,形式化方法的实践,目前，各种网络软件标准协议已普遍采用形式化方法进行描述，原因是采用朴素的非形式方式，规范中常常存在许多漏洞，存在许多不一致的或者不准确的地方（互联网规范特别不能容忍这类问题）具体例子包括：RBAC(基于角色的访问控制模型)规范（Z描述，2004）W3C WSDL 2.0规范（Z描述，2005）W3C XQuery 1.0 and XPath 2.0 Formal Semantics（结构化操作语义，2005）,软件形式化方法展望,形式化方法在过去的30多年里已经取得了巨大的进步，然而它在许多方面还需要更多的研究和努力。在计算机科学理论各方面的进展均会直接或间接推动形式化方法的发展，加强形式化工具的易用性和集成性。同时和其它工具结合形成一个集成的开发环境，使工业界更愿意接受形式化方法。将来，形式化方法将会融入到信息技术的各个领域，成为一种主流的方法和技术。,