形式化方法引论

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

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

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

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

5、loyd、Hoare和Manna等开展的程序正确性证明研究推动了形式化方法的发展，他们试图用数学方法来证明程序的正确性并发展成为了各种程序验证方法，但是受程序规模的限制，这些方法并未达到预期的应用效果。,形式化方法的发展,20世纪80年代，在硬件设计领域形式化方法的工业应用结果掀起了软件形式化开发方法的学术研究和工业应用的热潮。Pnueh提出了反应式系统规格和验证的时态逻辑（TemporalLogic，TL）方法。Clarke和Emerson提出了有穷状态并发系统的模型检验(ModelChecking)方法。,形式化方法的发展,经过几十年的研究和应用，形式化方法取得了大量、重要的成果从早期最简

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

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

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

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

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

11、e/Two等进程代数语言CSP、CCS、演算等；时序逻辑语言PLTL、CTL、XYZ/E、UNITY、TLA等；这些规约语言由于基于不同的数学理论及规约方法，因而也千差万别，但它们有一个共同的特点,即每种规约语言均由基本成分和构造成分两部分构成。前者用来描述基本(原子)规约,后者把基本部分组合成大规约。构造成分是形式规约研究和设计的重点，也是衡量规约语言优劣的主要依据。,一个简化的生命周期模型,定义软件需求文档SRD在完成需求搜集和分析之后，得到了软件需求文档SRD。它可被当作客户与软件提供者之间的合同。定义软件需求规格或行为规格(BS)软件需求规格（或行为规格）在不去考虑系统的具体实现方法的

12、前提下，描述了系统所期望的是什么。它以SRD中所声明的对象为基础，根据从外部可观察到的系统功能特征，来对所期望的系统行为进行准确和明确的描述。如果存在对系统的约束，也可将其作为系统的特征来进行说明。,一个简化的生命周期模型,定义设计规格(DS)设计规格在保持需求规格所声明的特征的前提下，指明系统的运行特点和内部结构。并可能根据一些具体需要，提供实现其行为的机制。设计规格与行为规格相比，增加了更多的细节。然而必须确保这些细节不改变需求规格所定义的系统的外部行为。通过增加越来越多的数据、行为、控制，以及异常描述等方面的细节，设计规格细化软件需求规格，并对需求规格进行更具体地描述。,一个简化的生命周

13、期模型,对于设计规格中的每一个组件，可以更加详细地指定组件的界面和组件间的交互，并进一步细化成一系列的规格。从而得到界面规格和详细设计规格或程序规格(PS)。详细设计规格可以用程序来实现。,规格可以采用非形式化的方式描述，包括自然语言、图、表等，也可以采用形式化方式描述。由于非形式化方法本身所存在的矛盾、二义性、含糊性，以及描述规格时的不完整性、抽象层次混杂等情况，使得所得到的规格不能准确地刻画系统模型，甚至会为后来的软件开发埋下出错的隐患。,形式化方法由于基于严格的数学基础，具有严格的语法和语义定义，从而可以准确地描述系统模型，排除了矛盾、二义性、含糊性等情况。在对系统进行严格地描述的过程中

14、，将会帮助开发人员和用户明确那些原本模糊的需求，并发现用户所陈述的需求中存在的矛盾，有利于相对完整、正确地理解用户需求，最终得到一个完整、正确的系统模型。,形式化规格精确地描述了用户的需求、软件系统的功能以及各种性质，其描述的是“做什么”，而不考虑“怎么做”。在书写规格时应该注意的一个问题是：如何描述得恰如其分，既不过多也不过少。在规格中描述过多会导致“实现偏向”，给实现施加了不必要的限制，从而排除了一些原本是合理的实现。描述得过少又有容纳不合理实现的危险。为了开发出良好的规格，除了应透彻理解、熟练掌握所使用的形式规格语言和方法外，还应对所要描述的系统有全面深入的了解。,已建立了多种适用于软件

15、系统规格的形式化方法，可分为三类：操作类描述类双重类操作类方法基于状态和转移，通过可执行模型来描述系统，模型本身能够采用静态分析和模型执行而得到验证，这类方法包括有限状态机、Statecharts、Petri网等。,描述类方法基于数学公理和概念，通过逻辑或代数给出系统的状态空间，具有高度抽象的特点，便于通过自动工具进行验证。基于不同的数学基础，描述类方法进一步分为：基于代数的描述类方法，如Z、VDM、Larch等。基于逻辑的描述类方法，如命题线性时态逻辑(PropositionalLinearTemporalLogic，PLTL)一阶线性时态逻辑(FirstOrderLinearTernpor

16、alLogic，PLTL)计算树逻辑(ComputationTreeTemporalLogic，CTTL)等时态逻辑为代表,双重类方法则兼有前面二者的特点，既能够通过数学公理和概念来高度抽象地描述系统，又具有状态和转移的可执行特征。这类方法包括：扩展状态机实时时态逻辑(ExtendedStateMachineReal一TimeTemporalLogic，ESMRTTL)TRIO+TROL等,20世纪80年代，牛津大学和Hursley实验室合作将Z方法，用于开发IBM商用信息控制系统。IBM对整个开发所进行的测试表明：明显地改善了产品质量大量地减少了错误和早期诊断错误其总体开发成本降低了9（IB

17、M估计）这一成果荣获皇家技术成就奖,Praxis公司于1992年开发了英国民航局的信息显示系统伦敦机场新空中交通管理系统的一部分在该系统的需求分析阶段，形式化规格和非形式结构化的需求概念相结合。在系统规格阶段，采用了抽象的VDM模型。在设计阶段，抽象VDM模型被细化为更具体的模块化规格。,Praxis公司这个项目开发的生产效率与采用非形式化技术相当、甚至更好。软件质量得到了很大的提高软件的故障率仅为0.75每千行代码，大大低于采用非形式化技术所开发出的软件系统的故障率（约为220每千行代码）,美国加州大学的安全关键系统研究组所开发的空中交通防碰撞系统的形式化需求规格TCASII，采用了基于St

18、atecharts的需求状态机语言RSML，解决了开发过程中遇到的许多问题。TCASH项目表明复杂过程控制系统软件开发采用形式化需求规格的可能性应用工程师们不经任何专门培训建立易读且易评判的形式化规格的可行性（注：Statecharts相对容易）,形式化规格还在如下方面得到了应用,数据库：用于存储病人监护信息的HP医用仪器实时数据库系统电子仪器：Tektronix系列谐波发生器、Schlumberger家用电度计硬件：INMOS浮点处理器、INMOS中T9000系列的虚拟信道处理器医疗设备：核磁共振理疗系统核反应堆系统：核反应器安全系统、核发电系统的切换装置,形式化规格还在如下方面得到了应用,

19、保密系统：NATO控制指挥和控制系统中的保密策略模型、Multinet网关系统的数据安全传输、美国国家标准和技术院的令牌访问控制系统电信系统：AT&T的5ESS电话交换系统、德国电信的电话业务系统运输系统：巴黎地铁的自动火车保护系统、英国铁路信号控制、以色列机载航空电子软件。,形式化验证,软件开发中的绝大部分错误是在需求分析和规格的早期阶段引入的，这些错误将随着开发的深入而逐渐放大。并且，这些错误发现得越晚，对其修改所需付出的代价也将会越大。在传统的软件开发方法中，除了在各个开发阶段进行评审以发现错误外，更多的错误则是直到编码结束后的测试阶段才能被检测出。形式化方法在开发出形式规格后就进行形式

20、验证。实际上是使得验证工作得以提前进行，既可以提前发现错误，同时在修改所发现的错误时需要付出的代价也是最小的。,形式化验证,形式化验证的主要技术包括模型检验和定理证明模型检验是一种基于有限状态模型并检验该模型的期望特性的技术。模型检验就是对模型的状态空间进行蛮力搜索，以确认该系统模型是否具有某些性质。搜索的可终止性依赖于模型的有限性。模型检验主要适用于有穷状态系统。,形式化验证,模型检验的优点完全自动化并且验证速度快当所检验的性质未被满足时，将终止搜索过程并给出反例。这种信息常常反映了系统设计中的失误，因而对于用户排错有极大的帮助。模型检验可用于系统的部分规格，即对于只给出了部分规格的系统，通

21、过搜索也可以提供关于已知部分正确性的有用信息。,形式化验证,模型检验方法的一个严重缺陷是“状态爆炸问题”。即，随着所要检验的系统的规模增大，模型检验算法所需的时间空间开销往往呈指数增长，因而极大地限制了其实际使用范围。有序二叉决策图(OrderedBinaryDecisionDiagrams，OBDD)是表述状态转移系统的高效率方法，使得较大规模系统的验证成为可能。模型检验可以处理100至200个状态变量的系统。模型检验已用来检验状态数目可达10120的系统。并且通过采用适当的抽象技术，就可以处理具有更多状态的系统。,形式化验证,模型检验离不开模型检验工具的支持。已有的模型检验工具可分为时态逻

22、辑模型检验工具行为一致检验工具复合检验工具。时态逻辑模型检验工具有EMC、CESAR、SMV、Murphi、SPIN、UV、SVE、HyTech、Kronos等行为一致检验工具有CospanFormalllCheck、FDR等；复合检验工具有HSIS、VIS、STeP、METAFrame等。,形式化验证,贝尔实验室在FormalCheck下，对其高级数据链路控制器进行了模型检验，以验证功能。他们对6个性能进行了规格，其中5个验证无误，另外一个失败，从而进一步发现了一个影响信道流量的Bug。楼宇抗震分布式主动结构控制系统的设计规格的系统模型有2.121019数目的状态。经过模型检验，自动分析并发

23、现了影响主动控制效果的计时器设置错误。,形式化验证,基于SMV输入语言建立了IEEEFuturebus+896.1一1991标准下cache一致协议的精确模型，通过SMV验证了转移系统模型满足cache一致性的规格。从中发现了先前并未找到和潜在的协议设计中的错误。Murphi有限状态模型检验工具对IEEE标准1596一1992下cache一致协议进行了验证，发现了变量、逻辑等方面的错误。,形式化验证,Philips公司音响设备的控制协议通过HyTech得到了完全自动验证，这是一个具有离散和连续特征的混杂系统的验证问题。对AT&T公司的7500条通信软件的SDL源代码进行了验证，从中发现112个

24、错误，约55的初始设计需求在逻辑上不一致。,形式化验证定理证明,定理证明采用逻辑公式来规格系统及其性质。逻辑公式由一个具有公理和推理规则的形式化系统给出。进行定理证明的过程就是应用这些公理或推理规则来证明系统具有某些性质。不同于模型检验，定理证明可以处理无限状态空间问题。,形式化验证定理证明,定理证明系统可分为自动和交互式两种类型。自动定理证明系统是通用搜索过程，在解决各种组合问题中比较成功。交互式定理证明系统需要与用户进行交互，要求用户能提供验证中创造性最强部分(建立断言等)的工作，因而其效率较低，较难用于大系统的验证。,形式化验证定理证明,定理证明的的实施同样需要定理证明器的支持。现有的定

25、理证明器包括：用户导引自动推演工具证明检验器复合证明器,形式化验证定理证明,用户导引自动推演工具有ACL2、Eves、LP、Nqthm、Reve和RRI这些工具由引理或者定义序列导引，每一个定理采用已建立的推演和引理，进行自动证明。证明检验器有Coq、HOL、LEGO、LCF和Nuprl复合证明器Analytica中将定理证明和符号代数系统Mathematica复合，PVS和Step将决策过程、模型检验和交互式证明复合在一体。,形式化验证定理证明,基于符号代数运算的自动定理证明用于证明Pentium中SRT算法的正确性，检查出了一个错误。ACL2用于AMD5K86的浮点除微代码的规格和机械证明

26、，ACL2还用来检验浮点方根微的代码的正确性，发现了其中的Bug，并对修改后的微代码进行了正确性的机器证明。ACL2用于Motorola复数算术处理器CSP的完全规格，同时对CSP的几个算法进行了验证。PVS用于航空电子微处理器AAMP5的规格和验证，对209条AAMP5指令中的108条进行了规格，验证了11个有代表性的微代码。,程序求精,程序求精又称为程序变换，是将自动推理和形式化方法相结合而形成的一门技术。它研究从抽象的形式规格推演出具体的面向计算机的程序代码的全过程。程序求精的基本思想是用一个抽象程度低、过程性强的程序去代替一个抽象程度高、过程性弱的程序，并保持它们之问功能的一致性。这里

27、所说的“程序”与传统观点中“可以由计算机直接执行”的“程序”不同，这里的“程序”是对规格、设计文档，以及程序代码的统称。,程序求精,因此，“程序”可以划分为若干层次最高层是不能直接执行的程序，即规格，它由抽象的描述语句构成。最低层是可以直接执行的程序，称为程序代码，它由可执行的命令语句构成。最高层和最低层之间为一系列混合程序，其中既含有抽象的描述语句，又含有可执行的命令语句。,程序求精,程序开发过程实际上就是从最高层的程序开始，通过一系列的求精变换步骤，每一步都降低一些抽象程度或增加一些可执行性，最终得到能够指导计算机明确执行的程序代码。在进行求精的过程中要注意保证程序的正确性，即保证所得到的

28、程序是满足最初的形式规格的。程序的这种正确性可以通过求精过程中所遵循的一系列规则来保证，也可以在事后采用验证工具来证明。,程序求精,程序求精技术是形式化方法研究的一个热点。在已出现的许多相关技术中，真正能够应用到实际软件开发过程中的并不多。目前比较典型的是IBMHursley公司和牛津大学PRG程序设计研究组提出的针对Z规格的求精方法，以及CarrollMogan的规则求精方案。,程序求精,形式化开发方法一直受到多方面的争议，这些争议主要体现在：形式化方法中所包含的数学理论，限制了大多数程序设计人员的学习和使用。采用形式化方法会延误项目开发周期，增加开发费用。许多流行的形式化方法对于较小规模项

29、目是有效的，但却很难应用于大型项目。形式化方法不能确保开发出完全正确的软件缺乏对软件生命周期内各个阶段提供全面支持的形式化方法等。,程序求精,形式化方法中的抽象数学符号及理论确实给软件工程师的使用带来一些不便，以致于人们要花时间和精力去学习和掌握。但是，采用形式化方法可以极大地减少系统设计开发早期阶段的错误，避免后期错误修改所带来的高额成本开销。采用形式化方法还会提高系统的开发效率。并且形式化方法是高质量、高可靠性软件开发的有效途径，是软件自动化的根本前提。,程序求精,形式化方法不会完全代替非形式化的软件开发方法，软件工程师们需要根据所解决问题的特点结合或选择使用。,程序求精,形式化方法结合到

30、具体的软件开发过程中需要考虑如下一些因素：应用的类型：形式化方法不可能对所有的应用类型都适用。对于一个项目，应该衡量其问题领域的特点以及模型的复杂性，从而确定是否适于采用形式化方法。,程序求精,规模和结构：在将形式化方法用于一个项目之前，还应该评价项目的规模和结构复杂性。形式化方法可有效地适用于中等规模的系统。为了使大型系统能充分受益于所采用的形式化方法，该系统应该具有很好的结构，并能分解成定义良好的构件，从而使其中的关键部分只受形式化方法的控制。类型的选择：在将形式化方法用于一个项目时，必须能清楚地确定其目标。不同的应用目的将对开发过程产生不同的影响，从而影响到对形式化方法类型的选择。,程序

31、求精,形式化级别：对一个系统可能进行非形式化、半形式化或者高度形式化的描述。从某个给定项目的目标出发，必须先确定其应用的关键程度、项目规模、可用的资源，以及对项目合适的形式化程度等，并从这些可能性中做出一个选择。使用范围：虽然形式化方法可使用于开发过程的所有阶段，但通常只是有选择地使用。一方面需要对形式化方法所应用于的开发阶段进行选择，另一方面，需要对采用形式化方法的构件进行选择。对那些决定安全性的构件不但需要形式化，而且需要高度的形式化。,程序求精,工具：为了足够精确地实施形式化方法，工具的支持是必须的。,程序求精,形式化方法在软件产业中应用的深入有赖于诸多方面工作的进展。需要开发出将整体特性分解为易于验证的局部特性的有效方法大规模复杂软件中搜索空间是巨大的，需要研究新的处理方法形式化方法与非形式化方法的结合形式化方法和新的软件开发技术（如SOA）的结合需要有效的软件工具,程序求精,具有良好用户界面、容易学习和