形式化方法引论.ppt

《形式化方法引论.ppt》由会员分享，可在线阅读，更多相关《形式化方法引论.ppt（72页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、软件开发的形式化方法引论软件开发的形式化方法引论目录单击此处添加标题文字单击此处添加标题文字单击此处添加文字内容单击此处添加文字内容 单击此处添加文字内容单击此处添加文字内容 单击此处添加文字内容单击此处添加文字内容单击此处添加标题文字单击此处添加标题文字单击此处添加文字内容单击此处添加文字内容 单击此处添加文字内容单击此处添加文字内容 单击此处添加文字内容单击此处添加文字内容单击此处添加标题文字单击此处添加标题文字单击此处添加文字内容单击此处添加文字内容 单击此处添加文字内容单击此处添加文字内容 单击此处添加文字内容单击此处添加文字内容单击此处添加标题文字单击此处添加标题文字单击此处添加文字

2、内容单击此处添加文字内容 单击此处添加文字内容单击此处添加文字内容 单击此处添加文字内容单击此处添加文字内容形式化方法形式化方法形式化方法(formal methods)(formal methods)在逻辑科学中是指分析、研究思维形式结构的在逻辑科学中是指分析、研究思维形式结构的方法。方法。它能精确地揭示各种逻辑规律它能精确地揭示各种逻辑规律,制定相应的逻制定相应的逻辑规则辑规则,使各种理论体系更加严密。使各种理论体系更加严密。也能正确地训练思维、提高思维的抽象能力。也能正确地训练思维、提高思维的抽象能力。软件工程方法的一种分类软件工程方法可以按照在软件开发中应用数学的严格程度（即形式化程度

3、），进行分类。完全非形式化的方法：指运用图、文本、表格和简单符号等，去建立各种软件模型。其中不使用数学。完全形式化的方法：以具有良好数学基础和数学表示形式的形式化规格语言，建立各种软件模型。完全非形式化的方法的缺陷各种模型中很容易包含具有矛盾、歧义、含糊、不完整的内容。也容易产生抽象程度的混杂。形式化方法的优点形式化方法支持抽象，利于建模形式化方法是准确的，利于减除模糊和歧义形式化方法是精确的，利于提高简洁和清晰形式化方法是严格的，利于提高正确性形式化方法支持推理，利于检测矛盾和不完整形式化方法能够提供高层的描述和验证手段形式化方法形式化方法(Formal Method)(Formal Met

4、hod)的基本含义是借助数的基本含义是借助数学的方法来研究计算机科学中的有关问题。学的方法来研究计算机科学中的有关问题。定义：定义：“用于开发计算机系统的形式化方法是基用于开发计算机系统的形式化方法是基于数学的用于描述系统性质的技术。这样的形式于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框架，人们可以在该框架中以化方法提供了一个框架，人们可以在该框架中以系统的方式刻画、开发和验证系统系统的方式刻画、开发和验证系统”。软件形式化方法的定义软件形式化方法基于良好的数学基础，提供了一个框架，在软件形式化方法基于良好的数学基础，提供了一个框架，在框架中可以用系统的而不是特别的方式刻划、开

5、发和验证软框架中可以用系统的而不是特别的方式刻划、开发和验证软件系统。件系统。形式化方法的本质是基于数学的方法来描述目标软件系形式化方法的本质是基于数学的方法来描述目标软件系统属性统属性不同的形式化方法的数学基础是不同的不同的形式化方法的数学基础是不同的有的以集合论和一阶谓词演算为基础（如有的以集合论和一阶谓词演算为基础（如Z Z和和VDMVDM）有的以时态逻辑为基础有的以时态逻辑为基础数学基础提供了一系列精确定义的概念数学基础提供了一系列精确定义的概念一致性一致性完整性完整性正确性正确性 形式化方法需要形式化规约说明语言的支持形式化方法需要形式化规约说明语言的支持在软件开发的全过程中，凡是采

6、用严格的数学语言，具有精确的数学语义的方法，都称为形式化方法。从广义角度，形式化方法是软件开发过程中分析、设计及实现的系统工程方法。从狭义角度，形式化方法是软件规格(Specification)和验证(Verification)的方法。因此，形式化方法又分为形式化规格方法和形式化验证方法。形式化规格是通过具有明确数学定义的文法和语义的方法或语言对软件的期望特性或者行为进行的精确、简洁描述。形式化验证是基于已建立的形式化规格，对软件的相关特性进行评价的数学分析和证明。形式化方法的发展软件的形式化开发方法，最早可追溯到软件的形式化开发方法，最早可追溯到2020世纪世纪5050年代后期对程序设计语言

7、编译技术的研究。年代后期对程序设计语言编译技术的研究。出现了形式化说明和验证编译程序的各种方法出现了形式化说明和验证编译程序的各种方法J.BackusJ.Backus提出提出BNFBNF描述描述Algol60Algol60语言的语法语言的语法出现了各种语法分析程序自动生成器以及语法制导的出现了各种语法分析程序自动生成器以及语法制导的编译方法，编译方法，使得编译系统的开发从使得编译系统的开发从“手工艺制作方式手工艺制作方式”发展发展成具有牢固理论基础的系统方法。成具有牢固理论基础的系统方法。形式化方法的发展在在2020世纪世纪6060年代，面对当时出现的软件危机，年代，面对当时出现的软件危机，F

8、loydFloyd、HoareHoare和和MannaManna等开展的程序正确性证明研等开展的程序正确性证明研究推动了形式化方法的发展，他们试图用数学方究推动了形式化方法的发展，他们试图用数学方法来证明程序的正确性并发展成为了各种程序验法来证明程序的正确性并发展成为了各种程序验证方法，但是受程序规模的限制，这些方法并未证方法，但是受程序规模的限制，这些方法并未达到预期的应用效果。达到预期的应用效果。形式化方法的发展2020世纪世纪8080年代，在硬件设计领域形式化方法的工年代，在硬件设计领域形式化方法的工业应用结果掀起了软件形式化开发方法的学术研业应用结果掀起了软件形式化开发方法的学术研究和

9、工业应用的热潮。究和工业应用的热潮。PnuehPnueh提出了反应式系统规格和验证的时态逻提出了反应式系统规格和验证的时态逻辑（辑（Temporal LogicTemporal Logic，TLTL）方法。）方法。ClarkeClarke和和EmersonEmerson提出了有穷状态并发系统的提出了有穷状态并发系统的模型检验模型检验(Model Checking)(Model Checking)方法。方法。形式化方法的发展经过几十年的研究和应用，形式化方法取得了大经过几十年的研究和应用，形式化方法取得了大量、重要的成果量、重要的成果从早期最简单的形式化方法从早期最简单的形式化方法一阶谓词演算一

10、阶谓词演算方法到现在的应用于不同领域、不同阶段的基方法到现在的应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程代数、代数等众于逻辑、状态机、网络、进程代数、代数等众多形式化方法多形式化方法形式化方法逐渐融入软件开发过程的各个阶段形式化方法逐渐融入软件开发过程的各个阶段,从需求分析、功能描述从需求分析、功能描述(规约规约)、(体系结构体系结构/算算法法)设计、编程、测试直至维护。设计、编程、测试直至维护。形式化方法的发展近年来，形式化方法的研究及其在工业中的应用近年来，形式化方法的研究及其在工业中的应用得到了长足的发展。得到了长足的发展。研究人员建立了系统设计人员易于理解的规格研究人员建立

11、了系统设计人员易于理解的规格概念和术语，以及有效应用这些术语和概念的概念和术语，以及有效应用这些术语和概念的形式化规格方法及语言，形式化规格方法及语言，建立了功能更加强大和完善的模型检验和定理建立了功能更加强大和完善的模型检验和定理证明技术。证明技术。开发出了与之相应的从研究原型到商品化产品开发出了与之相应的从研究原型到商品化产品的支撑工具和环境。的支撑工具和环境。将形式化方法用于软件开发的主要目的是保证软将形式化方法用于软件开发的主要目的是保证软件的正确性。件的正确性。形式化方法基于严格的数学，而在软件开发过程形式化方法基于严格的数学，而在软件开发过程中使用数学具有如下优点：中使用数学具有如

12、下优点：数学是准确的建模媒体，能够对现象、对象、动作等数学是准确的建模媒体，能够对现象、对象、动作等进行简洁、准确地描述。进行简洁、准确地描述。数学支持抽象，它使得规格的本质可以被展示出来，数学支持抽象，它使得规格的本质可以被展示出来，并且还可以以一种有组织的方式来表示系统规格中的并且还可以以一种有组织的方式来表示系统规格中的抽象层次。抽象层次。数学提供了高层确认的手段，可以使用数学证明，来数学提供了高层确认的手段，可以使用数学证明，来揭示规格中的矛盾性和不完整性，以及用来展示设计揭示规格中的矛盾性和不完整性，以及用来展示设计和规格之间的一致情况等。和规格之间的一致情况等。形式化规格说明涉及的

13、主要概念形式化方法为系统的数据和功能，定义了数据不变式、状态和操作。数据不变式一组条件表达式，每个条件在包含一组数据的系统的执行过程中总应保持为真状态是从系统的外部能够观察到的行为模式的一种表示，或者是系统访问和修改的存储数据操作系统中发生的动作，以及对状态数据的读写。形式化规格说明涉及的主要概念与操作相关的三种类型的条件不变式前置条件：定义操作执行前须满足的前提条件后置条件：定义操作执行后需满足的条件。通过定义操作对数据影响效果的方式来表达形式化软件开发方法采用了软件生命周期的变换形式化软件开发方法采用了软件生命周期的变换模型。从某种角度上，形式化软件开发方法实际模型。从某种角度上，形式化软

14、件开发方法实际上就是把现实世界的需求反映成软件的模型化过上就是把现实世界的需求反映成软件的模型化过程。程。在进行模型化的过程中涉及到三方面的系统模型在进行模型化的过程中涉及到三方面的系统模型现实世界现实世界模型表示模型表示计算机系统计算机系统形式化软件开发方法的过程就是从这三方面对系形式化软件开发方法的过程就是从这三方面对系统进行描述和转换的过程。统进行描述和转换的过程。开发过程中的任务依次分为开发过程中的任务依次分为模型获取模型获取模型验证模型验证模型变换模型变换模型获取是从现实世界向模型表示转换的过程，模型获取是从现实世界向模型表示转换的过程，包括如何提取出模型以及如何表示模型，它对应包括

15、如何提取出模型以及如何表示模型，它对应于软件生命周期中的需求分析、规格，以及设计于软件生命周期中的需求分析、规格，以及设计等活动。等活动。模型验证是对所得到的模型表示进行检验，判断模型验证是对所得到的模型表示进行检验，判断其是否捕获了所有的用户需求，以及该模型是否其是否捕获了所有的用户需求，以及该模型是否具有所期望的特性。具有所期望的特性。模型变换是从模型表示向计算机系统变换的过程，模型变换是从模型表示向计算机系统变换的过程，一个抽象的模型表示可以变换到各种计算机系统一个抽象的模型表示可以变换到各种计算机系统环境上。环境上。模型变换对应于软件生命周期中的实现和测试等模型变换对应于软件生命周期中

16、的实现和测试等活动。这些任务分别对应于如下三方面的活动：活动。这些任务分别对应于如下三方面的活动：形式化规格形式化规格形式化验证形式化验证程序求精程序求精(Refinement)(Refinement)在模型变换时的一个关键任务是进行一致性测试。在模型变换时的一个关键任务是进行一致性测试。即判断在变换后所得到的计算机系统是否与模型即判断在变换后所得到的计算机系统是否与模型表示相一致。表示相一致。形式规约形式规约形式规约形式规约(Formal Specification,(Formal Specification,也称形式规范也称形式规范或形式化描述或形式化描述)它是对程序它是对程序“做什么做什

17、么”(what to do)(what to do)的数学描的数学描述述,是用具有精确语义的形式语言书写的程序功是用具有精确语义的形式语言书写的程序功能描述能描述,它是设计和编制程序的出发点它是设计和编制程序的出发点,也是验也是验证程序是否正确的依据。证程序是否正确的依据。对形式规约通常要讨论其一致性对形式规约通常要讨论其一致性(自身无矛盾自身无矛盾)和完备性和完备性(是否完全、无遗漏地刻画所要描述的是否完全、无遗漏地刻画所要描述的对象对象)等性质。等性质。形式规约形式规约形式规约的方法主要可分为两类形式规约的方法主要可分为两类:一类是面向模型的方法也称为系统建模一类是面向模型的方法也称为系统

18、建模,该方该方法通过构造系统的计算模型来刻画系统的不同法通过构造系统的计算模型来刻画系统的不同行为特征；行为特征；另一类是面向性质的方法也称为性质描述另一类是面向性质的方法也称为性质描述,该该方法通过定义系统必须满足的一些性质来描述方法通过定义系统必须满足的一些性质来描述一个系统。一个系统。形式规约形式规约不同的形式规约方法要求不同的形式规约语言不同的形式规约方法要求不同的形式规约语言,即用于书即用于书写形式规约的语言写形式规约的语言(也称形式化描述语言也称形式化描述语言),),代数语言代数语言OBJOBJ、ClearClear、ASLASL、ACT One/TwoACT One/Two等等进

19、程代数语言进程代数语言CSPCSP、CCSCCS、演算等；演算等；时序逻辑语言时序逻辑语言PLTLPLTL、CTLCTL、XYZ/EXYZ/E、UNITYUNITY、TLATLA等；等；这些规约语言由于基于不同的数学理论及规约方法，这些规约语言由于基于不同的数学理论及规约方法，因而也千差万别，但它们有一个共同的特点因而也千差万别，但它们有一个共同的特点,即每种规即每种规约语言均由基本成分和构造成分两部分构成。前者用约语言均由基本成分和构造成分两部分构成。前者用来描述基本来描述基本(原子原子)规约规约,后者把基本部分组合成大规约。后者把基本部分组合成大规约。构造成分是形式规约研究和设计的重点，也

20、是衡量规构造成分是形式规约研究和设计的重点，也是衡量规约语言优劣的主要依据。约语言优劣的主要依据。一个简化的生命周期模型定义软件需求文档定义软件需求文档SRDSRD在完成需求搜集和分析之后，得到了软件需求文档在完成需求搜集和分析之后，得到了软件需求文档SRDSRD 。它可被当作客户与软件提供者之间的合同。它可被当作客户与软件提供者之间的合同。定义软件需求规格或行为规格定义软件需求规格或行为规格(BS)(BS)软件需求规格（或行为规格）在不去考虑系统的具体软件需求规格（或行为规格）在不去考虑系统的具体实现方法的前提下，描述了系统所期望的是什么。实现方法的前提下，描述了系统所期望的是什么。它以它以

21、SRDSRD中所声明的对象为基础，根据从外部可观察到中所声明的对象为基础，根据从外部可观察到的系统功能特征，来对所期望的系统行为进行准确和的系统功能特征，来对所期望的系统行为进行准确和明确的描述。明确的描述。如果存在对系统的约束，也可将其作为系统的特征来如果存在对系统的约束，也可将其作为系统的特征来进行说明。进行说明。一个简化的生命周期模型定义设计规格定义设计规格(DS)(DS)设计规格在保持需求规格所声明的特征的前提下，指设计规格在保持需求规格所声明的特征的前提下，指明系统的运行特点和内部结构。并可能根据一些具体明系统的运行特点和内部结构。并可能根据一些具体需要，提供实现其行为的机制。需要，

22、提供实现其行为的机制。设计规格与行为规格相比，增加了更多的细节。然而设计规格与行为规格相比，增加了更多的细节。然而必须确保这些细节不改变需求规格所定义的系统的外必须确保这些细节不改变需求规格所定义的系统的外部行为。部行为。通过增加越来越多的数据、行为、控制，以及异常描通过增加越来越多的数据、行为、控制，以及异常描述等方面的细节，设计规格细化软件需求规格，并对述等方面的细节，设计规格细化软件需求规格，并对需求规格进行更具体地描述。需求规格进行更具体地描述。一个简化的生命周期模型对于设计规格中的每一个组件，可以更加详细地对于设计规格中的每一个组件，可以更加详细地指定组件的界面和组件间的交互，并进一

23、步细化指定组件的界面和组件间的交互，并进一步细化成一系列的规格。从而得到界面规格和详细设计成一系列的规格。从而得到界面规格和详细设计规格或程序规格规格或程序规格(PS)(PS)。详细设计规格可以用程序来实现。详细设计规格可以用程序来实现。规格可以采用非形式化的方式描述，包括自然语规格可以采用非形式化的方式描述，包括自然语言、图、表等，也可以采用形式化方式描述。言、图、表等，也可以采用形式化方式描述。由于非形式化方法本身所存在的矛盾、二义性、由于非形式化方法本身所存在的矛盾、二义性、含糊性，以及描述规格时的不完整性、抽象层次含糊性，以及描述规格时的不完整性、抽象层次混杂等情况，使得所得到的规格不

24、能准确地刻画混杂等情况，使得所得到的规格不能准确地刻画系统模型，甚至会为后来的软件开发埋下出错的系统模型，甚至会为后来的软件开发埋下出错的隐患。隐患。形式化方法由于基于严格的数学基础，具有严格形式化方法由于基于严格的数学基础，具有严格的语法和语义定义，从而可以准确地描述系统模的语法和语义定义，从而可以准确地描述系统模型，排除了矛盾、二义性、含糊性等情况。型，排除了矛盾、二义性、含糊性等情况。在对系统进行严格地描述的过程中，将会帮助开在对系统进行严格地描述的过程中，将会帮助开发人员和用户明确那些原本模糊的需求，并发现发人员和用户明确那些原本模糊的需求，并发现用户所陈述的需求中存在的矛盾，有利于相

25、对完用户所陈述的需求中存在的矛盾，有利于相对完整、正确地理解用户需求，最终得到一个完整、整、正确地理解用户需求，最终得到一个完整、正确的系统模型。正确的系统模型。形式化规格精确地描述了用户的需求、软件系统形式化规格精确地描述了用户的需求、软件系统的功能以及各种性质，其描述的是的功能以及各种性质，其描述的是“做什么做什么”，而不考虑而不考虑“怎么做怎么做”。在书写规格时应该注意的一个问题是：如何描述在书写规格时应该注意的一个问题是：如何描述得恰如其分，既不过多也不过少。得恰如其分，既不过多也不过少。在规格中描述过多会导致在规格中描述过多会导致“实现偏向实现偏向”，给实现施加，给实现施加了不必要的

26、限制，从而排除了一些原本是合理的实现。了不必要的限制，从而排除了一些原本是合理的实现。描述得过少又有容纳不合理实现的危险。描述得过少又有容纳不合理实现的危险。为了开发出良好的规格，除了应透彻理解、熟练为了开发出良好的规格，除了应透彻理解、熟练掌握所使用的形式规格语言和方法外，还应对所掌握所使用的形式规格语言和方法外，还应对所要描述的系统有全面深入的了解。要描述的系统有全面深入的了解。已建立了多种适用于软件系统规格的形式化方法，已建立了多种适用于软件系统规格的形式化方法，可分为三类：可分为三类：操作类操作类描述类描述类双重类双重类操作类方法基于状态和转移，通过可执行模型来操作类方法基于状态和转移

27、，通过可执行模型来描述系统，模型本身能够采用静态分析和模型执描述系统，模型本身能够采用静态分析和模型执行而得到验证，这类方法包括有限状态机、行而得到验证，这类方法包括有限状态机、StatechartsStatecharts、PetriPetri网等。网等。描述类方法基于数学公理和概念，通过逻辑或代描述类方法基于数学公理和概念，通过逻辑或代数给出系统的状态空间，具有高度抽象的特点，数给出系统的状态空间，具有高度抽象的特点，便于通过自动工具进行验证。便于通过自动工具进行验证。基于不同的数学基础，描述类方法进一步分为：基于不同的数学基础，描述类方法进一步分为：基于代数的描述类方法，如基于代数的描述类

28、方法，如Z Z、VDMVDM、LarchLarch等。等。基于逻辑的描述类方法，如基于逻辑的描述类方法，如命题线性时态逻辑命题线性时态逻辑(Propositional Linear(Propositional Linear Temporal LogicTemporal Logic，PLTL)PLTL)一阶线性时态逻辑一阶线性时态逻辑(First(FirstOrder Linear Order Linear Ternporal LogicTernporal Logic，PLTL)PLTL)计算树逻辑计算树逻辑(Computation Tree Temporal Logic(Computation

29、 Tree Temporal Logic，CTTL)CTTL)等时态逻辑为代表等时态逻辑为代表双重类方法则兼有前面二者的特点，既能够通过双重类方法则兼有前面二者的特点，既能够通过数学公理和概念来高度抽象地描述系统，又具有数学公理和概念来高度抽象地描述系统，又具有状态和转移的可执行特征。这类方法包括：状态和转移的可执行特征。这类方法包括：扩展状态机实时时态逻辑扩展状态机实时时态逻辑(Extended State Machine(Extended State MachineRealReal一一Time Temporal LogicTime Temporal Logic，ESMESMRTTL)RTT

30、L)TRIO+TRIO+TROLTROL等等2020世纪世纪8080年代，牛津大学和年代，牛津大学和HursleyHursley实验室合作将实验室合作将Z Z方法，用于开发方法，用于开发IBMIBM商用信息控制系统。商用信息控制系统。IBMIBM对整个开发所进行的测试表明：对整个开发所进行的测试表明：明显地改善了产品质量明显地改善了产品质量大量地减少了错误和早期诊断错误大量地减少了错误和早期诊断错误其总体开发成本降低了其总体开发成本降低了9 9 （IBMIBM估计）估计）这一成果荣获皇家技术成就奖这一成果荣获皇家技术成就奖PraxisPraxis公司于公司于19921992年开发了英国民航局的

31、信息显年开发了英国民航局的信息显示系统示系统伦敦机场新空中交通管理系统的一部分伦敦机场新空中交通管理系统的一部分在该系统的需求分析阶段，形式化规格和非形式在该系统的需求分析阶段，形式化规格和非形式结构化的需求概念相结合。在系统规格阶段，采结构化的需求概念相结合。在系统规格阶段，采用了抽象的用了抽象的VDMVDM模型。模型。在设计阶段，抽象在设计阶段，抽象VDMVDM模型被细化为更具体的模块模型被细化为更具体的模块化规格。化规格。PraxisPraxis公司这个项目开发的生产效率与采用非形公司这个项目开发的生产效率与采用非形式化技术相当、甚至更好。式化技术相当、甚至更好。软件质量得到了很大的提高

32、软件质量得到了很大的提高软件的故障率仅为软件的故障率仅为0.750.75每千行代码，大大低于采用非每千行代码，大大低于采用非形式化技术所开发出的软件系统的故障率（约为形式化技术所开发出的软件系统的故障率（约为2 22020每千行代码）每千行代码）美国加州大学的安全关键系统研究组所开发的空美国加州大学的安全关键系统研究组所开发的空中交通防碰撞系统的形式化需求规格中交通防碰撞系统的形式化需求规格TCASIITCASII，采，采用了基于用了基于StatechartsStatecharts的需求状态机语言的需求状态机语言RSMLRSML，解，解决了开发过程中遇到的许多问题。决了开发过程中遇到的许多问题

33、。TCASHTCASH项目表明项目表明复杂过程控制系统软件开发采用形式化需求规格的可复杂过程控制系统软件开发采用形式化需求规格的可能性能性应用工程师们不经任何专门培训建立易读且易评判的应用工程师们不经任何专门培训建立易读且易评判的形式化规格的可行性（注：形式化规格的可行性（注：StatechartsStatecharts相对容易）相对容易）形式化规格还在如下方面得到了应用数据库：用于存储病人监护信息的数据库：用于存储病人监护信息的HPHP医用仪器实医用仪器实时数据库系统时数据库系统电子仪器：电子仪器：TektronixTektronix系列谐波发生器、系列谐波发生器、SchlumbergerS

34、chlumberger家用电度计家用电度计硬件：硬件：INMOSINMOS浮点处理器、浮点处理器、INMOSINMOS中中T9000T9000系列的虚系列的虚拟信道处理器拟信道处理器医疗设备：核磁共振理疗系统医疗设备：核磁共振理疗系统核反应堆系统：核反应器安全系统、核发电系统核反应堆系统：核反应器安全系统、核发电系统的切换装置的切换装置形式化规格还在如下方面得到了应用保密系统：保密系统：NATONATO控制指挥和控制系统中的保密策控制指挥和控制系统中的保密策略模型、略模型、MultinetMultinet网关系统的数据安全传输、美网关系统的数据安全传输、美国国家标准和技术院的令牌访问控制系统国

35、国家标准和技术院的令牌访问控制系统电信系统：电信系统：AT&TAT&T的的5ESS5ESS电话交换系统、德国电信电话交换系统、德国电信的电话业务系统的电话业务系统运输系统：巴黎地铁的自动火车保护系统、英国运输系统：巴黎地铁的自动火车保护系统、英国铁路信号控制、以色列机载航空电子软件。铁路信号控制、以色列机载航空电子软件。形式化验证 软件开发中的绝大部分错误是在需求分析和规格软件开发中的绝大部分错误是在需求分析和规格的早期阶段引入的，这些错误将随着开发的深入的早期阶段引入的，这些错误将随着开发的深入而逐渐放大。并且，这些错误发现得越晚，对其而逐渐放大。并且，这些错误发现得越晚，对其修改所需付出的

36、代价也将会越大。修改所需付出的代价也将会越大。在传统的软件开发方法中，除了在各个开发阶段在传统的软件开发方法中，除了在各个开发阶段进行评审以发现错误外，更多的错误则是直到编进行评审以发现错误外，更多的错误则是直到编码结束后的测试阶段才能被检测出。码结束后的测试阶段才能被检测出。形式化方法在开发出形式规格后就进行形式验证。形式化方法在开发出形式规格后就进行形式验证。实际上是使得验证工作得以提前进行，既可以提实际上是使得验证工作得以提前进行，既可以提前发现错误，同时在修改所发现的错误时需要付前发现错误，同时在修改所发现的错误时需要付出的代价也是最小的。出的代价也是最小的。形式化验证形式化验证的主要

37、技术包括模型检验和定理证明形式化验证的主要技术包括模型检验和定理证明模型检验是一种基于有限状态模型并检验该模型模型检验是一种基于有限状态模型并检验该模型的期望特性的技术。的期望特性的技术。模型检验就是对模型的状态空间进行蛮力搜索，模型检验就是对模型的状态空间进行蛮力搜索，以确认该系统模型是否具有某些性质。搜索的可以确认该系统模型是否具有某些性质。搜索的可终止性依赖于模型的有限性。终止性依赖于模型的有限性。模型检验主要适用于有穷状态系统。模型检验主要适用于有穷状态系统。形式化验证模型检验的优点模型检验的优点完全自动化并且验证速度快完全自动化并且验证速度快当所检验的性质未被满足时，将终止搜索过程并

38、给出当所检验的性质未被满足时，将终止搜索过程并给出反例。这种信息常常反映了系统设计中的失误，因而反例。这种信息常常反映了系统设计中的失误，因而对于用户排错有极大的帮助。对于用户排错有极大的帮助。模型检验可用于系统的部分规格，即对于只给出了部模型检验可用于系统的部分规格，即对于只给出了部分规格的系统，通过搜索也可以提供关于已知部分正分规格的系统，通过搜索也可以提供关于已知部分正确性的有用信息。确性的有用信息。形式化验证模型检验方法的一个严重缺陷是模型检验方法的一个严重缺陷是“状态爆炸问题状态爆炸问题”。即，随着所要检验的系统的规模增大，模型。即，随着所要检验的系统的规模增大，模型检验算法所需的时

39、间空间开销往往呈指数增长，检验算法所需的时间空间开销往往呈指数增长，因而极大地限制了其实际使用范围。因而极大地限制了其实际使用范围。有序二叉决策图有序二叉决策图(Ordered Binary Decision(Ordered Binary Decision DiagramsDiagrams，OBDD)OBDD)是表述状态转移系统的高效率方是表述状态转移系统的高效率方法，使得较大规模系统的验证成为可能。法，使得较大规模系统的验证成为可能。模型检验可以处理模型检验可以处理100100至至200200个状态变量的系统。个状态变量的系统。模型检验已用来检验状态数目可达模型检验已用来检验状态数目可达10

40、10120120的系统。的系统。并且通过采用适当的抽象技术，就可以处理具有并且通过采用适当的抽象技术，就可以处理具有更多状态的系统。更多状态的系统。形式化验证模型检验离不开模型检验工具的支持。模型检验离不开模型检验工具的支持。已有的模型检验工具可分为已有的模型检验工具可分为时态逻辑模型检验工具时态逻辑模型检验工具行为一致检验工具行为一致检验工具复合检验工具。复合检验工具。时态逻辑模型检验工具有时态逻辑模型检验工具有EMCEMC、CESARCESAR、SMVSMV、MurphiMurphi、SPINSPIN、UVUV、SVESVE、HyTechHyTech、KronosKronos等等行为一致检

41、验工具有行为一致检验工具有CospanCospanFormalllCheckFormalllCheck、FDRFDR等；等；复合检验工具有复合检验工具有HSISHSIS、VISVIS、STePSTeP、METAFrameMETAFrame等。等。形式化验证贝尔实验室在贝尔实验室在FormalCheckFormalCheck下，对其高级数据链路下，对其高级数据链路控制器进行了模型检验，以验证功能。他们对控制器进行了模型检验，以验证功能。他们对6 6个个性能进行了规格，其中性能进行了规格，其中5 5个验证无误，另外一个失个验证无误，另外一个失败，从而进一步发现了一个影响信道流量的败，从而进一步发现

42、了一个影响信道流量的BugBug。楼宇抗震分布式主动结构控制系统的设计规格的楼宇抗震分布式主动结构控制系统的设计规格的系统模型有系统模型有2.12102.12101919数目的状态。经过模型检验，数目的状态。经过模型检验，自动分析并发现了影响主动控制效果的计时器设自动分析并发现了影响主动控制效果的计时器设置错误。置错误。形式化验证基于基于SMVSMV输入语言建立了输入语言建立了IEEE Futurebus+896.1IEEE Futurebus+896.1一一19911991标准下标准下cachecache一致协议的精确模型，通过一致协议的精确模型，通过SMVSMV验证了转移系统模型满足验证了

43、转移系统模型满足cachecache一致性的规格。从一致性的规格。从中发现了先前并未找到和潜在的协议设计中的错中发现了先前并未找到和潜在的协议设计中的错误。误。MurphiMurphi有限状态模型检验工具对有限状态模型检验工具对IEEEIEEE标准标准15961596一一19921992下下cachecache一致协议进行了验证，发现了变量、一致协议进行了验证，发现了变量、逻辑等方面的错误。逻辑等方面的错误。形式化验证PhilipsPhilips公司音响设备的控制协议通过公司音响设备的控制协议通过HyTechHyTech得到得到了完全自动验证，这是一个具有离散和连续特征了完全自动验证，这是一个

44、具有离散和连续特征的混杂系统的验证问题。的混杂系统的验证问题。对对AT&TAT&T公司的公司的75007500条通信软件的条通信软件的SDLSDL源代码进行了源代码进行了验证，从中发现验证，从中发现112112个错误，约个错误，约5555的初始设计需的初始设计需求在逻辑上不一致。求在逻辑上不一致。形式化验证定理证明定理证明采用逻辑公式来规格系统及其性质。逻定理证明采用逻辑公式来规格系统及其性质。逻辑公式由一个具有公理和推理规则的形式化系统辑公式由一个具有公理和推理规则的形式化系统给出。进行定理证明的过程就是应用这些公理或给出。进行定理证明的过程就是应用这些公理或推理规则来证明系统具有某些性质。

45、推理规则来证明系统具有某些性质。不同于模型检验，定理证明可以处理无限状态空不同于模型检验，定理证明可以处理无限状态空间问题。间问题。形式化验证定理证明定理证明系统可分为自动和交互式两种类型。定理证明系统可分为自动和交互式两种类型。自动定理证明系统是通用搜索过程，在解决各种自动定理证明系统是通用搜索过程，在解决各种组合问题中比较成功。组合问题中比较成功。交互式定理证明系统需要与用户进行交互，要求交互式定理证明系统需要与用户进行交互，要求用户能提供验证中创造性最强部分用户能提供验证中创造性最强部分(建立断言等建立断言等)的工作，因而其效率较低，较难用于大系统的验的工作，因而其效率较低，较难用于大系

46、统的验证。证。形式化验证定理证明定理证明的的实施同样需要定理证明器的支持。定理证明的的实施同样需要定理证明器的支持。现有的定理证明器包括：现有的定理证明器包括：用户导引自动推演工具用户导引自动推演工具证明检验器证明检验器复合证明器复合证明器形式化验证定理证明用户导引自动推演工具有用户导引自动推演工具有ACL2ACL2、EvesEves、LPLP、NqthmNqthm、ReveReve和和RRIRRI这些工具由引理或者定义序列导引，这些工具由引理或者定义序列导引，每一个定理采用已建立的推演和引理，进行自动证明。每一个定理采用已建立的推演和引理，进行自动证明。证明检验器有证明检验器有CoqCoq、

47、HOLHOL、LEGOLEGO、LCFLCF和和NuprlNuprl复合证明器复合证明器AnalyticaAnalytica中将定理证明和符号代数系中将定理证明和符号代数系统统MathematicaMathematica复合，复合，PVSPVS和和StepStep将决策过程、模将决策过程、模型检验和交互式证明复合在一体。型检验和交互式证明复合在一体。形式化验证定理证明基于符号代数运算的自动定理证明用于证明基于符号代数运算的自动定理证明用于证明PentiumPentium中中SRTSRT算法的正确性，检查出了一个错误。算法的正确性，检查出了一个错误。ACL2ACL2用于用于AMD5K86AMD5

48、K86的浮点除微代码的规格和机械证的浮点除微代码的规格和机械证明，明，ACL2ACL2还用来检验浮点方根微的代码的正确性，还用来检验浮点方根微的代码的正确性，发现了其中的发现了其中的BugBug，并对修改后的微代码进行了正，并对修改后的微代码进行了正确性的机器证明。确性的机器证明。ACL2ACL2用于用于MotorolaMotorola复数算术处理器复数算术处理器CSPCSP的完全规格，的完全规格，同时对同时对CSPCSP的几个算法进行了验证。的几个算法进行了验证。PVSPVS用于航空电子微处理器用于航空电子微处理器AAMP5AAMP5的规格和验证，的规格和验证，对对209209条条AAMP5

49、AAMP5指令中的指令中的108108条进行了规格，验证了条进行了规格，验证了1111个有代表性的微代码。个有代表性的微代码。程序求精程序求精又称为程序变换，是将自动推理和形式程序求精又称为程序变换，是将自动推理和形式化方法相结合而形成的一门技术。它研究从抽象化方法相结合而形成的一门技术。它研究从抽象的形式规格推演出具体的面向计算机的程序代码的形式规格推演出具体的面向计算机的程序代码的全过程。的全过程。程序求精的基本思想是用一个抽象程度低、过程程序求精的基本思想是用一个抽象程度低、过程性强的程序去代替一个抽象程度高、过程性弱的性强的程序去代替一个抽象程度高、过程性弱的程序，并保持它们之问功能的

50、一致性。程序，并保持它们之问功能的一致性。这里所说的这里所说的“程序程序”与传统观点中与传统观点中“可以由计算可以由计算机直接执行机直接执行”的的“程序程序”不同，这里的不同，这里的“程序程序”是对规格、设计文档，以及程序代码的统称。是对规格、设计文档，以及程序代码的统称。程序求精因此，因此，“程序程序”可以划分为若干层次可以划分为若干层次最高层是不能直接执行的程序，即规格，它由抽象的最高层是不能直接执行的程序，即规格，它由抽象的描述语句构成。描述语句构成。最低层是可以直接执行的程序，称为程序代码，它由最低层是可以直接执行的程序，称为程序代码，它由可执行的命令语句构成。可执行的命令语句构成。最