形式化方法引论

《形式化方法引论》由会员分享，可在线阅读，更多相关《形式化方法引论（72页珍藏版）》请在金锄头文库上搜索。

1、软件开发的形式化方法引论,目录,形式化方法,形式化方法(formal methods) 在逻辑科学中是指分析、研究思维形式结构的方法。 它能精确地揭示各种逻辑规律,制定相应的逻辑规则,使各种理论体系更加严密。 也能正确地训练思维、提高思维的抽象能力。,软件工程方法的一种分类,软件工程方法可以按照在软件开发中应用数学的严格程度（即形式化程度），进行分类。 完全非形式化的方法：指运用图、文本、表格和简单符号等，去建立各种软件模型。其中不使用数学。 完全形式化的方法：以具有良好数学基础和数学表示形式的形式化规格语言，建立各种软件模型。,完全非形式化的方法的缺陷,各种模型中很容易包含具有矛盾、歧义、含

2、糊、不完整的内容。 也容易产生抽象程度的混杂。,形式化方法的优点,形式化方法支持抽象，利于建模 形式化方法是准确的，利于减除模糊和歧义 形式化方法是精确的，利于提高简洁和清晰 形式化方法是严格的，利于提高正确性 形式化方法支持推理，利于检测矛盾和不完整形式化方法能够提供高层的描述和验证手段,形式化方法(Formal Method)的基本含义是借助数学的方法来研究计算机科学中的有关问题。 定义：“用于开发计算机系统的形式化方法是基于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框架，人们可以在该框架中以系统的方式刻画、开发和验证系统”。,软件形式化方法的定义,软件形式化方法基于良好的数

3、学基础，提供了一个框架，在框架中可以用系统的而不是特别的方式刻划、开发和验证软件系统。 形式化方法的本质是基于数学的方法来描述目标软件系统属性 不同的形式化方法的数学基础是不同的 有的以集合论和一阶谓词演算为基础（如Z和VDM） 有的以时态逻辑为基础 数学基础提供了一系列精确定义的概念 一致性 完整性 正确性 形式化方法需要形式化规约说明语言的支持,在软件开发的全过程中，凡是采用严格的数学语言，具有精确的数学语义的方法，都称为形式化方法。 从广义角度，形式化方法是软件开发过程中分析、设计及实现的系统工程方法。 从狭义角度，形式化方法是软件规格(Specification)和验证(Verific

4、ation)的方法。因此，形式化方法又分为形式化规格方法和形式化验证方法。,形式化规格是通过具有明确数学定义的文法和语义的方法或语言对软件的期望特性或者行为进行的精确、简洁描述。 形式化验证是基于已建立的形式化规格，对软件的相关特性进行评价的数学分析和证明。,形式化方法的发展,软件的形式化开发方法，最早可追溯到20世纪50年代后期对程序设计语言编译技术的研究。 出现了形式化说明和验证编译程序的各种方法 J.Backus提出BNF描述Algol60语言的语法 出现了各种语法分析程序自动生成器以及语法制导的编译方法， 使得编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法。,形式化

5、方法的发展,在20世纪60年代，面对当时出现的软件危机，Floyd、Hoare和Manna等开展的程序正确性证明研究推动了形式化方法的发展，他们试图用数学方法来证明程序的正确性并发展成为了各种程序验证方法，但是受程序规模的限制，这些方法并未达到预期的应用效果。,形式化方法的发展,20世纪80年代，在硬件设计领域形式化方法的工业应用结果掀起了软件形式化开发方法的学术研究和工业应用的热潮。 Pnueh提出了反应式系统规格和验证的时态逻辑（Temporal Logic，TL）方法。 Clarke和Emerson提出了有穷状态并发系统的模型检验(Model Checking)方法。,形式化方法的发展,

6、经过几十年的研究和应用，形式化方法取得了大量、重要的成果 从早期最简单的形式化方法一阶谓词演算方法到现在的应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程代数、代数等众多形式化方法形式化方法逐渐融入软件开发过程的各个阶段,从需求分析、功能描述(规约)、(体系结构/算法)设计、编程、测试直至维护。,形式化方法的发展,近年来，形式化方法的研究及其在工业中的应用得到了长足的发展。 研究人员建立了系统设计人员易于理解的规格概念和术语，以及有效应用这些术语和概念的形式化规格方法及语言， 建立了功能更加强大和完善的模型检验和定理证明技术。 开发出了与之相应的从研究原型到商品化产品的支撑工具和环境。,

7、将形式化方法用于软件开发的主要目的是保证软件的正确性。 形式化方法基于严格的数学，而在软件开发过程中使用数学具有如下优点： 数学是准确的建模媒体，能够对现象、对象、动作等进行简洁、准确地描述。 数学支持抽象，它使得规格的本质可以被展示出来，并且还可以以一种有组织的方式来表示系统规格中的抽象层次。 数学提供了高层确认的手段，可以使用数学证明，来揭示规格中的矛盾性和不完整性，以及用来展示设计和规格之间的一致情况等。,形式化规格说明涉及的主要概念,形式化方法为系统的数据和功能，定义了数据不变式、状态和操作。数据不变式 一组条件表达式，每个条件在包含一组数据的系统的执行过程中总应保持为真 状态 是从系

8、统的外部能够观察到的行为模式的一种表示，或者是系统访问和修改的存储数据 操作 系统中发生的动作，以及对状态数据的读写。,形式化规格说明涉及的主要概念,与操作相关的三种类型的条件 不变式 前置条件：定义操作执行前须满足的前提条件 后置条件：定义操作执行后需满足的条件。通过定义操作对数据影响效果的方式来表达,形式化软件开发方法采用了软件生命周期的变换模型。从某种角度上，形式化软件开发方法实际上就是把现实世界的需求反映成软件的模型化过程。 在进行模型化的过程中涉及到三方面的系统模型 现实世界 模型表示 计算机系统,形式化软件开发方法的过程就是从这三方面对系统进行描述和转换的过程。 开发过程中的任务依

9、次分为 模型获取 模型验证 模型变换,模型获取是从现实世界向模型表示转换的过程，包括如何提取出模型以及如何表示模型，它对应于软件生命周期中的需求分析、规格，以及设计等活动。 模型验证是对所得到的模型表示进行检验，判断其是否捕获了所有的用户需求，以及该模型是否具有所期望的特性。,模型变换是从模型表示向计算机系统变换的过程，一个抽象的模型表示可以变换到各种计算机系统环境上。 模型变换对应于软件生命周期中的实现和测试等活动。这些任务分别对应于如下三方面的活动： 形式化规格 形式化验证 程序求精(Refinement) 在模型变换时的一个关键任务是进行一致性测试。即判断在变换后所得到的计算机系统是否与

10、模型表示相一致。,形式规约,形式规约(Formal Specification,也称形式规范或形式化描述) 它是对程序“做什么”(what to do)的数学描述,是用具有精确语义的形式语言书写的程序功能描述,它是设计和编制程序的出发点,也是验证程序是否正确的依据。 对形式规约通常要讨论其一致性(自身无矛盾)和完备性(是否完全、无遗漏地刻画所要描述的对象)等性质。,形式规约,形式规约的方法主要可分为两类: 一类是面向模型的方法也称为系统建模,该方法通过构造系统的计算模型来刻画系统的不同行为特征； 另一类是面向性质的方法也称为性质描述,该方法通过定义系统必须满足的一些性质来描述一个系统。,形式规

11、约,不同的形式规约方法要求不同的形式规约语言,即用于书写形式规约的语言(也称形式化描述语言), 代数语言OBJ、Clear、ASL、ACT One/Two等 进程代数语言CSP、CCS、演算等； 时序逻辑语言PLTL、CTL、XYZ/E、UNITY、TLA等； 这些规约语言由于基于不同的数学理论及规约方法，因而也千差万别，但它们有一个共同的特点,即每种规约语言均由基本成分和构造成分两部分构成。前者用来描述基本(原子)规约,后者把基本部分组合成大规约。构造成分是形式规约研究和设计的重点，也是衡量规约语言优劣的主要依据。,一个简化的生命周期模型,定义软件需求文档SRD 在完成需求搜集和分析之后，得

12、到了软件需求文档SRD 。它可被当作客户与软件提供者之间的合同。 定义软件需求规格或行为规格(BS) 软件需求规格（或行为规格）在不去考虑系统的具体实现方法的前提下，描述了系统所期望的是什么。 它以SRD中所声明的对象为基础，根据从外部可观察到的系统功能特征，来对所期望的系统行为进行准确和明确的描述。 如果存在对系统的约束，也可将其作为系统的特征来进行说明。,一个简化的生命周期模型,定义设计规格(DS) 设计规格在保持需求规格所声明的特征的前提下，指明系统的运行特点和内部结构。并可能根据一些具体需要，提供实现其行为的机制。 设计规格与行为规格相比，增加了更多的细节。然而必须确保这些细节不改变需

13、求规格所定义的系统的外部行为。 通过增加越来越多的数据、行为、控制，以及异常描述等方面的细节，设计规格细化软件需求规格，并对需求规格进行更具体地描述。,一个简化的生命周期模型,对于设计规格中的每一个组件，可以更加详细地指定组件的界面和组件间的交互，并进一步细化成一系列的规格。从而得到界面规格和详细设计规格或程序规格(PS)。 详细设计规格可以用程序来实现。,规格可以采用非形式化的方式描述，包括自然语言、图、表等，也可以采用形式化方式描述。 由于非形式化方法本身所存在的矛盾、二义性、含糊性，以及描述规格时的不完整性、抽象层次混杂等情况，使得所得到的规格不能准确地刻画系统模型，甚至会为后来的软件开

14、发埋下出错的隐患。,形式化方法由于基于严格的数学基础，具有严格的语法和语义定义，从而可以准确地描述系统模型，排除了矛盾、二义性、含糊性等情况。 在对系统进行严格地描述的过程中，将会帮助开发人员和用户明确那些原本模糊的需求，并发现用户所陈述的需求中存在的矛盾，有利于相对完整、正确地理解用户需求，最终得到一个完整、正确的系统模型。,形式化规格精确地描述了用户的需求、软件系统的功能以及各种性质，其描述的是“做什么”，而不考虑“怎么做”。 在书写规格时应该注意的一个问题是：如何描述得恰如其分，既不过多也不过少。 在规格中描述过多会导致“实现偏向”，给实现施加了不必要的限制，从而排除了一些原本是合理的实

15、现。 描述得过少又有容纳不合理实现的危险。 为了开发出良好的规格，除了应透彻理解、熟练掌握所使用的形式规格语言和方法外，还应对所要描述的系统有全面深入的了解。,已建立了多种适用于软件系统规格的形式化方法，可分为三类： 操作类 描述类 双重类 操作类方法基于状态和转移，通过可执行模型来描述系统，模型本身能够采用静态分析和模型执行而得到验证，这类方法包括有限状态机、Statecharts、Petri网等。,描述类方法基于数学公理和概念，通过逻辑或代数给出系统的状态空间，具有高度抽象的特点，便于通过自动工具进行验证。 基于不同的数学基础，描述类方法进一步分为： 基于代数的描述类方法，如Z、VDM、L

16、arch等。 基于逻辑的描述类方法，如 命题线性时态逻辑(Propositional Linear Temporal Logic，PLTL) 一阶线性时态逻辑(FirstOrder Linear Ternporal Logic，PLTL) 计算树逻辑(Computation Tree Temporal Logic，CTTL)等时态逻辑为代表,双重类方法则兼有前面二者的特点，既能够通过数学公理和概念来高度抽象地描述系统，又具有状态和转移的可执行特征。这类方法包括： 扩展状态机实时时态逻辑(Extended State MachineReal一Time Temporal Logic，ESMRTTL) TRIO+ TROL等,20世纪80年代，牛津大学和Hursley实验室合作将Z方法，用于开发IBM商用信息控制系统。 IBM对整个开发所进行的测试表明： 明显地改善了产品质量 大量地减少了错误和早期诊断错误 其总体开发成本降低了9 （IBM估计） 这一成果荣获皇家技术成就奖,Praxis公司于1992年开发了英国民航局的信息显示系统 伦敦机场新空中交通管理系统的一部分 在该系统的需求分析阶段，形式化规格和非形式结构化的需求概念相结合。在系统规格阶段，采用了抽象的VDM模型。 在设计阶段，抽象VDM模型被细化为更具体的模块化规格。,