软件开发的形式化方法.ppt

软件开发的形式化方法硕士研究生讲义周清雷 郑州大学信息工程学院,课程参考教材,参考材料软件开发的形式化方法，古天龙编，2005，高等教育出版社软件可靠性方法，Doron A.Peled著，王林章等译，2012，机械工业出版社,-2-,第1章 软件及其开发概述,-4-,内容安排,软件开发的历史软件危机软件工程形式化开发方法,-5-,1.1 软件开发的历史,软件软件开发把现实世界的需求反映成软件的模型化并予以实现的过程软件及开发的三个阶段程序设计阶段（1946年-1956年）科学计算、机器语言及汇编语言、个体编程编程技巧、程序效率没有文档、软件一词尚未出现,1.1 软件开发的历史,软件及开发的三个阶段程序系统阶段（1956年-1968年）1956年，J.Backus(77)Fortran语言诞生大量数据处理、小组开发“软件”一词出现：程序及其说明60年代中期，软件危机。IBM OS/360 P.Brooks软件工程阶段（1968年以来）1968年NATO会议，提出“软件工程”术语工程化方法、描述语言、团队开发软件的定义 当它被执行时能够提供所要求的功能和性能的指令或计算机程序 使得该程序能够满意地处理信息的数据结构 描述程序的功能需求以及程序的操作和使用文档,-6-,1.2 软件危机,1968年，NATO会议提出了“软件危机”一词软件危机包含两方面问题如何开发软件，以满足不断增长、日趋复杂的需求；如何维护数量不断膨胀的软件产品。软件危机主要表现如下几个方面开发成本昂贵项目进度难控质量无法保证修改维护困难,-7-,开发成本昂贵,1968年，美国花费于软件的投资高达60亿美元，有些系统，特别是军用系统，软费用要高出硬件费用好几倍，例如美国全球军事指挥控制系统的计算机硬件费用为1亿美元，而软件费用高达7.2亿美元。1980年美国政府的财政年度当中，计算机系统方面(软，硬件与服务)共耗资达570亿美元，其中320亿美元(占总数的56)用于计算机软件方面(与同年的美国汽车行业进行简单的比较，美国是当时的世界第一汽车生产大国，汽车的年销售量为900万辆，总的销售额仅为720亿美元。技术的进步使得计算机硬件的成本持续降低，而软件成本则不断增长，软件成本在计算机系统总成本中所占的比例呈现日益扩大的趋势来自美国空军计算机系统的数据表明，1970年，软件费用约占总费用的60，1975年达到72，1980年达到80，1985年计达到85。这种增长的速度是惊人的。（1979年，美国的国防预算为1258亿美元，其中9%用于计算机领域，约113亿美元。在这113亿美元当中，91亿美元（约占80）用于软件投资。仅有22亿美元用于硬件设备）。,-8-,项目进度难控,在研究大型系统时，遇到越来越多的困难。有的系绞干脆失败了，损失了大量金钱和人力；有的系统虽然完成了，但性能不理想，或推迟了许多年，经费大大超过预算。如一个大项目负责人所说：“软件人员太像皇帝新衣故事中的裁缝了、当我来检查软件开发工作时；所得到的回答好像对我说我们正忙于编织这件带有魔法的织物。只要等一会儿，你就会看到这件织物是极其美丽的。但是我什么也看不到，什么也摸不到，也说不出任何一个有关的数字；没有任何办法得到一些信息说明事情确实进行的非常顺利，而且我已经知道许多人最终已经编织了一大堆昂贵的废物而离去，还有下少人最终什么也没有作出来。”为软件开发制定进度是根困难的事情：通常我们对一个任务根据其复杂性、工作量及进度要求安排人力。如有10人月的工作量，则由一个人完成需要10个月，由10个入完成则需要一个月。但这种工作量估计方式仅对各部分工作互下干扰的情况下才适用，例如当各部分工作尚能很好地划分时，安排由不同人完成不同部分的工作。但作为整体，尚需讨论合作，这种讨论交流活动就增加了工作量。软件系统的结构很复杂，各部分附加联系极大。增加更多人工作，往往不是缩短时间进度，而是会延缓进度。,-9-,项目进度难控,对于一项复杂的任务，通常难于通过增加人力来缩短开发时间。Brook提出的法则“在已拖延的软件项目上增加入力只会使其更难按期完成”。这对于一般的工业产品来说是难于想象的！1995年，美国共取消810亿美元的软件项目，其中31%未完取消，53%的项目延长一半时间，9%按期完成且不超期。1998年，美国企业应用项目不成功比率75%,其中28%的项目取消，40%无限拖长且资金超出预赛对于一项复杂的任务，通常难于通过增加人力来缩短开发时间。Brook提出的法则“在已拖延的软件项目上增加入力只会使其更难按期完成”。这对于一般的工业产品来说是难于想象的！,-10-,质量无法保证,1985年11月21日,由于计算机软件的错误,造成纽约银行与美联储电子结算系统收支失衡,发生了超额支付,而这个问题一直到晚上才被发现,纽约银行当日帐务出现了230亿的短款。Therac-25是加拿大原子能公司AECL和一家法国公司CGR联合开发的一种医疗设备，它产生的高能光束或电子流能够杀死人体毒瘤而不会伤害毒瘤附近的人体健康组织。在1985年6月到1987年1月，因为软件缺陷引发了6起由于电子流或X-光束的过量使用的医疗事故，造成4人死亡、2人重伤的严重后果。美国Florida州的福利救济系统用于处理数百万受抚养儿童、食品券、医疗援助等受资助家庭接受者的资格认证，其基于巨型机系统，支持84个数据库、1390个程序、12000多个终端和个人计算机。1992年，该系统的错误使得成千上万的人收到了他们无权收到的救济，而其他成千上万急需食品券的人却排着长队等待了好几天。该错误导致了多支付2.6亿美元以及少支付5800万美元医疗补助的后果。1996年，欧洲航天局阿丽亚娜5型（Ariane5）火箭在发射后40秒钟后发生爆炸，2名法国士兵当场死亡，损耗资产达10亿美元之巨，历时9年的航天计划因此严重受挫。爆炸原因在于惯性导航系统软件技术要求和设计的错误。2002年，美国商务部的国立标准技术研究所（NIST）的调查报告：“据推测，由于软件缺陷而引起的损失额每年高达595亿美元。这一数字相当于美国国内生产值的0.6%”,-11-,软件维护困难,软件的维护任务特别重。事实上，正式投入使用的商用软件，总是存在着一定数量的错误。随着时间的延伸，在不同的运行条件下，软件就会出现故障，就需要维护。这种维护与通常意义下的设备（硬件）维护是完全不同的。因为软件是逻辑元件，不是一种实物。软件故障是软件中的逻辑故障所造成的，不是硬件的“用旧”、“磨损”之类问题。软件维护不是更换某种备件，而是要纠正逻辑缺陷。当软件系统变得庞大，问题变得复杂时，常常会发生“纠正一个错误带来更多新的错误！”的问题。新的错误发现、运行环境的改变、用户提出新要求，软件需不断修改没有遵循标准、没有准确的文档，维护困难巨大。,-12-,软件危机的原因：复杂性,复杂性 规模的复杂性 结构的复杂性 环境的复杂性 领域的复杂性 交流的复杂性,-13-,软件规模的复杂性,随着计算机应用的日益广泛，需要开发的软件规模越来越庞大。以美国宇航局的软件系统为例：1963年，水星计划的软件系统约有 200万条指令；1967年，双子星座计划系统约为400万条指令；1973年，阿波罗计划系统达到1000万条指令；1979年，哥伦比亚航天飞机系统更是达到了4000万条指令。软件庞大的规模是引起技术上和心理上挫折的一个重要因素；此外，规模的复杂性引起了大量学习和理解上的负担。由于在需求分析及生成规格的阶段需要搜集和分析的信息数量非常巨大，从而可能会使得信息不正确或不完整，并且在审查阶段也未能检查出来。正如Leveson 所认为的：几乎所有与计算机过程控制系统有关的事故都是源于这类由软件规模因素所引起的错误。,-14-,结构的复杂性,结构复杂性体现在管理和技术两个方面。在管理方面，开发小组用来组织和管理开发活动时所采用的层次的宽度和深度，决定了用来管理系统的结构的复杂性；此外，软件开发机构内部的惯例和制度可能会改变各小组之间的信息流动，从而增加了结构复杂性。在技术方面，软件系统的模块结构愈加复杂，模块之间复杂的调用关系以及接口信息往往超过了人们所能接受的程度。这种结构的复杂性可以用模块之间的耦合度来衡量，耦合度反映了在需求变化的情况下，相应所需修改的模块的数量。,-15-,环境的复杂性,首先，运行中的软件总是受其所处环境的影响，在接收到外界环境的触发事件时，软件应该做出正确的响应。为了保证软件的可靠性，原则上必须对其所处环境有很好的理解，对外界环境可能产生的所有事件进行考虑，但这往往是难以办到的。其次，对于许多软件系统来说，人们往往缺乏对其所运行的环境特性的认识。许多系统只有当成功地运行于其环境时，才能对其环境进行很好的理解。再次，软件运行环境的多样性和异构性给软件开发者带来了更大的挑战。,-16-,领域的复杂性,软件中所操作的对象仅仅是对应用领域真实对象的模拟，因而软件开发者需要从现实世界中抽象出软件模型所需的部分，并以其为基础构建软件。但是对于有的应用领域来说，这些模拟只能是近似的。其原因可能是由于对应用领域对象的认识不完全，或者是由于该模型所具有的苛刻条件限制，或者两者兼而有之。对于一个应用工程来说，其中所使用的模型应该是具有合理的科学理论支持，并且经过良好测试的。然而在某些软件应用领域中，并不存在可以认知的模型，或者没有准确的模型来描绘相应的物理对象的几何、拓扑以及其它特征。在这种缺少准确认识的情况下，应用领域的某些方面很可能在软件中不能体现出来。同时，由于有的软件是根据近似的模型来构建的，因而这些模型不一定能反映事实情况。,-17-,交流的复杂性,由于软件庞大的规模、大量的内部结构、以及应用领域的不同属性等因素，在开发一个大型软件系统时所参与的不仅仅是单个的人，而是一个团队。该团队里的每个人参与开发过程中的一个或多个活动。此时，对于参与不同开发阶段的人来说，彼此之间明确的交流非常重要。一方面，由于结构的复杂性以及开发团队的庞大等原因，团队成员之间的交流非常困难；另一方面，成员之间在进行交流时使用的媒介往往是自然语言、图、表等非形式化的方式，这些媒介很难准确地描述出所开发的产品的基本属性，并且，由于这些媒介本身所具有的二义性，往往会使开发人员产生错误的理解，这种错误将会随着开发过程的进行而逐渐蔓延开来，最终导致灾难性的后果。,-18-,软件危机？,软件危机的原因缺乏指导或实施软件设计、开发、维护的有效理论、方法及技术 或者缺乏有效解决软件设计、开发、维护中相关实际问题的理论、方法及技术 解决方案软件工程：工程的方法组织和管理形式化方法：正确性和可靠性,-19-,1.3 软件工程,NATO、软件工程的定义1983年IEEE给软件工程下的定义是：“软件工程是开发、远行、维护和修复软件的系统方法”。主要强调软件工程是系统方法而不是某种神秘的个人技巧。Fairly认为：“软件工程学是为了在成本限额以内按时完成开发和修改软件产品所需要的系统生产和维护技术及管理学科。”软件工程的目标：成本限额、按时完成，软件工程包含技术和管理。Fritz Bauer给出了下述定义：“软件工程是为了经济地获得可靠的且能在实际机器上有效运行的软件，而建立和使用的完善的工程化原则。”不仅指出软件工程的目标是经济地开发出高质量的软什，而且强调了软件工程是一门工程学科，应建立并使用完善的工程化原则。1993年IEEE进一步给出了一个更全面的定义“软件工程是：把系统化的、规范的、可度量的途径应用于软件并发、运行和维护的过程，也就是把工程化应用于软件中；研究中提到的途径。”,-20-,软件工程目标、内容,目标成功地生产具有正确性、可用性以及开销合宜的产品。三要素方法：构造软件的技术工具：自动化、半自动化的支持过程：综合运用方法和工具分步内容软件工程过程、生命周期、开发模型、开发方法、工具开发环境、计算机辅助软件工程、软件工程经济学,-21-,软件工程过程,规定了获取、供应、开发、操作以及维护软件时，所需要实施的过程、活动和任务。包括：开发过程：分析、设计、编码、集成、测试、安装和验收管理过程：范围定义、计划、实施和控制、评审评价、完成供应过程：供方按合同提供系统、软件、服务获取过程：需方操作过程：运行系统维护过程：修改支持过程：生命周期的支持,-22-,软件生命周期,五个活动需求分析和规格软件设计：逻辑模型转换为软件方案，总体结构、模块算法代码编写软件测试：模块测试、组装测试、确认测试运行维护,-23-,软件开发模型,组织软件生命周期内的各种活动：次序、任务、准则瀑布模型（Winston Royce 1970)计划任务书、需求规格、设计规格、程序、测试、维护缺点：需求分析的准确性问题、错误反馈不及时、进度难以控制原型模型快速成型、评估、反馈、改进缺点：用户不理解、开发人员的惰性不愿意优化,-24-,软件开发模型,螺旋模型（Barry W.Boehm,1988）制定计划、风险评估、实施工程、用户评价-演化缺点：丰富的评估经验和专业知识，要求高构件模型 即插即用编程标识、选用、组装，构件库优点：生产率、可靠、灵活、可维护,-25-,软件开发模型,四代技术模型（4GT)基于一系列软件工具的开发核心：规格软件的能力不支持软件开发的全过程侧重：设计阶段、实现阶段、支持界面缺点：维护问题变换模型基于形式化规格及程序变换的开发模型，自动程序设计模型或形式化方法模型三个核心活动：规格生成、形式化验证、计算机辅助程序求精高效、可靠、可控，但要求高,-26-,软件开发方法,软件开发方法是指在某种思想的指导下使用已经定义好的一系列技术和表示工具来组织软件开发过程的方法一般表述成一系列步骤典型的传统软件开发方法：结构化方法面向数据结构方法面向对象的开发方法,-27-,软件工具,辅助软件开发、维护和管理的一系列软件种类繁多管理工具、配置工具、分析设计工具、编码工具、测试工具测试工具：数据获取、静态分析、动态测试、模拟、测试管理维护工具：版本控制、文档分析、开发信息库、逆向过程等,-28-,软件开发环境,支持软件产品生产的软件系统，由软件工具和集成机制组成。软件工具集成机制：为工具集成和软件的开发、管理，以及维护提供统一的支持。前端开发环境、后端开发环境、软件维护环境、逆向工程环境,-29-,计算机辅助软件工程,实现软件生命周期各个环节的自动化整个生命周期的支持，解决生产效率软件工程经济学从经济学的观点来研究、分析如何有效地开发、发布软件产品和支持用户使用成本估算技术、模型、效益分析、多目标决策、不确定性的处理、风险分析、工期估计,-30-,1.4 形式化方法,形式化方法概念发展目的形式化方法软件开发 变换模型形式化规格形式化验证程序求精形式化方法的应用,-31-,形式化方法概念,形式化方法是渗透在软件生命期中各个环节（如：需求、设计、实现、测试等）的数学方法 或者 具有严格数学基础的软件开发方法形式化方法的基本含义是借助数学的方法来研究计算机科学中的有关问题。Encyclopedia of Software Engineering对形式化方法定义为：“用于开发计算机系统的形式化方法是基于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框架，人们可以在该框架中以系统的方式刻画、开发和验证系统”。,-32-,形式化方法概念,在软件开发的全过程中，凡是采用严格的数学语言，具有精确的数学语义的方法，都称为形式化方法。从广义角度，形式化方法是软件开发过程中分析、设计及实现的系统工程方法。狭义地，形式化方法是软件规格（specification）和验证（verification）的方法。形式化方法又分为形式化规格方法和形式化验证方法。形式化规格是通过具有明确数学定义的文法和语义的方法或语言对软件的期望特性或者行为进行的精确、简洁描述。形式化验证是基于已建立的形式化规格，对软件的相关特性进行评价的数学分析和证明。,-33-,发展历史,20世纪50年代后期，Backus（77）提出了巴克斯范式（Backus normal formula，简称BNF），作为描述程序设计语言语法的元语言；20世纪60年代，Floyd（78）、Hoare（80）和Manna等开展的程序正确性证明研究推动了形式化方法的发展，他们试图用数学方法来证明程序的正确性并发展成为了各种程序验证方法，但是受程序规模限制这些方法并未达到预期的应用效果；20世纪80年代，在硬件设计领域形式化方法的工业应用结果，掀起了软件形式化开发方法的学术研究和工业应用的热潮，Pnueli(96)提出了反应式系统规格和验证的时态逻辑(temporal logic，简称TL)方法，Clarke、Emerson、Sifakis(07)提出了有穷状态并发系统的模型检验(model checking)方法；近十年来，建立了易于理解的规格概念和术语、形式化规格方法及语言、形式化验证技术:模型检测和定理证明，开发了支撑工具和环境,-34-,形式化方法主要目标,形式化方法用于软件开发的主要目的是保证软件的正确性。形式化方法基于严格的数学，而在软件开发过程中使用数学具有如下优点：数学是准确的建模媒体，能够对现象、对象、动作等进行简洁、准确的描述；数学支持抽象，它使得规格的本质可以被展示出来，并且还可以以一种有组织的方式来表示系统规格中的抽象层次；数学提供了高层确认的手段，可以使用数学证明来揭示规格中的矛盾性和不完整性、以及用来展示设计和规格之间的一致情况等。（从软件工程知识体角度）2004年5月，IEEE-CS和ACM联合任务组提交了CCSE（Computing Curriculum-Software Engineering）最终报告，在该报告给出的SEEK（Software Engineering Education Knowledge）中，“软件的形式化方法（Formal Methods in Software Engineering）”被单列为一门必修课程（序列号为SE313）。,-36-,形式化方法软件开发,变化模型：把现实世界的需求反映成软件的模型化过程模型化涉及：现实世界、模型表示、计算机系统开发过程的任务分为：模型获取、模型验证、模型变换模型获取：从现实世界向模型表示转换，对应软件生命周期中的需求分析、规格、设计活动模型验证：是否满足需求及具有所期望的特性模型变换：从模型表示向计算机系统变换的过程。关键任务是一致性测试，对应软件生命周期中的实现和测试这些任务对应三方面的活动：形式化规格、形式化验证、程序求精,-37-,（1）形式化规格,软件规格是指对软件系统对象及用来对系统对象进行操作的方法集合，以及对所开发系统中的各对象在其生存期间里的集体行为的描述。软件生命周期模型将整个软件开发过程分解为一系列的阶段，并为每个阶段赋予明确的任务。“规格”应当理解为一个多阶段的、而不是仅仅某一个阶段的行为。,-38-,需求分析,系统设计I,程序开发,软件测试,软件运行,BS,codes,PS,DS,系统设计II,（1）形式化规格,规格可以采用非形式化的方式来描述，包括自然语言、图、表等，也可以采用形式化方式来描述。由于非形式化方法本身所存在的矛盾、二义性、含糊性，以及描述规格时的不完整性、抽象层次混杂等情况，使得所得到的规格不能准确地刻画系统模型，甚至会为后来的软件开发埋下出错的隐患。而对于形式化方法来说，由于其基于严格的数学，具有严格的语法和语义定义，从而可以准确地描述系统模型，排除了矛盾、二义性、含糊性等情况；同时，在对系统进行严格地描述的过程中，将会帮助用户明确其原本模糊的需求，并发现用户所陈述的需求中存在的矛盾等情况，从而相对完整、正确地理解用户需求，最终得到一个完整、正确的系统模型。,-39-,（1）形式化规格,形式规格精确地描述了用户的需求、软件系统的功能以及各种性质，其描述的是“做什么”，而不考虑“怎么做”。故在书写规格时应该注意的一个问题是如何描述得恰如其分，既不过多也不过少。在规格中描述过多会导致“实现偏向”，给实现施加了不必要的限制，从而排除了一些原本是合理的实现；描述得过少又有容纳不合理实现的危险。为了开发出良好的规格，除了应透彻理解、熟练掌握所使用的形式规格语言和方法外，更重要的是对所要描述的系统有全面深入的了解。,-40-,（1）形式化规格,形式化规约的分类:操作类方法：基于状态和转移，通过可执行模型来描述系统，模型本身能够采用静态分析和模型执行而得到验证，这类方法包括有限状态机、Statecharts、Petri网等描述类方法：基于数学公理和概念，通过逻辑或代数给出系统的状态空间，是高度抽象的，便于通过自动工具进行验证。包括基于代数的Z、VDM、Larch等方法，和基于时态逻辑的PLTL、FOLTL、CTTL方法双重类方法：兼有前面二者的特点，既能够通过数学公理和概念来高度抽象地描述系统，又具有状态和转移的可执行特征，这类方法包括扩展状态机/实时时态逻辑(ESM/RTTL)、TRIO+、TROL等,-41-,（1）形式化规格,形式化规格实例20世纪80年代，牛津大学和Hursley实验室于合作将Z用于IBM商用信息控制系统。IBM对整个开发所进行的测试表明：明显地改善了产品质量、大量地减少了错误和早期诊断错误。IBM估计使总体开发成本降低9。这一成果获皇家技术成就奖；1992年，Praxis公司交付给英国民航局的信息显示系统是伦敦机场新空中交通管理系统的部分。在系统规格阶段，采用了抽象的VDM模型。在设计阶段，抽象VDM细化为更为具体的模块化规格。项目开发的生产效率和采用非形式化技术相当、甚至更好。同时，软件质量得到了很大的提高，软件的故障率仅为0.75每千行代码，大大低于采用非形式化技术所提供的软件的故障率（约为220每千行代码）；美国加州大学的安全关键系统研究组所开发的空中交通防碰撞系统的形式化需求规格TCASII，采用了基于Statecharts的需求状态机语言RSML，解决了开发过程中遇到的许多问题。,-42-,（1）形式化规格,形式化规格实例其它方面的应用：数据库：用于存储病人监护信息的HP医用仪器实时数据库系统；电子仪器：Tektronix系列谐波发生器、Schlumberger家用电度计；硬件：INMOS浮点处理器、INMOS中T9000系列的虚拟信道处理器；医疗设备：核磁共振理疗系统；核反应堆系统：核反应器安全系统、核发电系统的切换装置；保密系统：NATO控制指挥和控制系统中的保密策略模型、Multinet网关系统的数据安全传输、美国国家标准和技术院的令牌访问控制系统；电信系统：AT&T的5ESS电话交换系统、德国电信的电话业务系统；运输系统：巴黎地铁的自动火车保护系统、英国铁路信号控制、以色列机载航空电子软件。,-43-,（2）形式化验证,主要技术：模型检测和定理证明模型检测模型检验是一种基于有限状态模型并检验该模型的期望特性的技术。粗略地讲，模型检验就是对模型的状态空间进行蛮力搜索，以确认该系统模型是否具有某些性质。搜索的可终止性依赖于模型的有限性。模型检验主要适用于有穷状态系统，其优点是完全自动化并且验证速度快；并且，模型检验可用于系统部分规格，即对于只给出了部分规格的系统，通过搜索也可以提供关于已知部分正确性的有用信息；此外，当所检验的性质未被满足时，将终止搜索过程并给出反例，这种信息常常反映了系统设计中的细微失误，因而对于用户排错有极大的帮助。模型检验方法的一个严重缺陷是“状态爆炸问题”，即随着所要检验的系统的规模增大，模型检验算法所需的时间/空间开销往往呈指数增长，因而极大限制了其实际使用范围。10120,-44-,（2）形式化验证,模型检测工具时态逻辑模型检验工具有EMC、CESAR、SMV、Mur、SPIN、UV、SVE、HyTech、Kronos等；行为一致检验工具有FDR、Cospan/Formal Check等；复合检验工具有HSIS、VIS、STeP、METAFrame等。模型检测实例贝尔实验室对其高级数据链路控制器在FormalCheck下进行了模型检验功能验证，6个性能进行了规格，其中5个验证无误、另外一个失败，从而进一步发现了一个影响信道流量的Bug；对某楼宇抗震分布式主动结构控制系统设计进行了规格，所生成的系统模型有2.121019数目的状态。经过模型检验分析发现了影响主动控制效果的计时器设置错误；,-45-,（2）形式化验证,模型检测实例基于SMV输入语言建立了IEEE Futurebus+896.1-1991标准下cache一致协议的精确模型，通过SMV验证了模型满足cache一致性的规格。并发现了先前并未找到的潜在协议设计错误。该工作是第一次从IEEE标准中发现错误；Philips公司音响设备的控制协议通过HyTech得到了完全自动验证，这是一个具有离散和连续特征的混杂系统验证问题；AT&T公司的7500条通信软件的SDL源代码进行了验证，从中发现112个错误，约55的初始设计需求在逻辑上不一致。,-46-,（2）形式化验证,定理证明采用逻辑公式来规格系统及其性质，其中的逻辑由一个具有公理和推理规则的形式化系统给出，进行定理证明的过程就是应用这些公理或推理规则来证明系统具有某些性质。不同于模型检验，定理证明可以处理无限状态空间问题。定理证明系统又可以粗略地分为自动和交互式两种类型。自动定理证明系统是通用搜索过程，在解决各种组合问题中比较成功；交互式定理证明系统需要与用户进行交互，要求用户能提供验证中创造性最强部分（建立断言等）的工作，因而其效率较低，较难用于大系统的验证。,-47-,（2）形式化验证,定理证明工具用户导引自动推演工具有ACL2、Eves、LP、Nqthm、Reve和RRL；证明检验器有Coq、HOL、LEGO、LCF和Nuprl；复合证明器Analytica、PVS和Step；定理证明实例基于符号代数运算的自动定理证明用于证明Pentium中SRT算法的正确性，检查出了一个由故障商数字选择表引起的错误；,-48-,（2）形式化验证,定理证明实例PowerPC和System/390中寄存器传输级、门级、晶体管级的硬件设计模拟为布尔状态转移函数，基于OBDD的算法用来检验不同设计级上状态转移函数的等价性；Nqthm用于Motorola 68020微处理器的规格，进而用来证明不同来源的二进制机器码的正确性；ACL2用于AMD5K86的浮点除微代码的规格和机械证明，ACL2还用来检验浮点方根微的正确性，发现了其中的Bug，并对修改后的微代码进行了正确性机械证明；ACL2用于Motorola复数算术处理器CSP的完全规格，同时对CSP的几个算法进行了验证；PVS用于航空电子微处理器AAMP5的规格和验证，对209条AAMP5指令中的108条进行了规格，验证了11个有代表性的微代码。,-49-,（3）程序求精,程序求精，又称为程序变换，是将自动推理和形式化方法相结合而形成的一门新技术，它研究从抽象的形式规格推演出具体的面向计算机的程序代码的全过程。程序求精的基本思想是用一个抽象程度低、过程性强的程序去代替一个抽象程度高、过程性弱的程序，并保持它们之间功能的一致。这里所说的“程序”与传统观点中“可以由计算机直接执行”的“程序”不同，这里的“程序”是对规格、设计文档以及程序代码的统称。在这种理解下，程序可以划分为若干层次：最高层是不能直接执行的程序，即规格，它由抽象的描述语句构成；最低层是可以直接执行的程序，称为程序代码，它由可执行的命令语句构成；最高层和最低层之间为一系列混合程序，其中既含有抽象的描述语句，又含有可执行的命令语句。,-50-,（3）程序求精,程序求精技术是形式化方法研究的一个热点，在已出现的许多相关技术中，真正能够应用到实际软件开发过程中的并不多。目前比较典型的是IBM Hursly公司以及牛津大学PRG程序设计研究组提出的针对Z规格的求精方法、以及Carroll Morgan的规则求精方案。,-51-,形式化方法争议,形式化方法一直受到多方面的争议持肯定态度的拥护者认为形式化方法会引起软件开发的革命，另一些持否定态度者则怀疑甚至反对将数学引入软件开发过程中。形式化方法的一些争议或缺陷主要体现在：形式化方法中所包含的数学理论，限制了大多数程序设计人员的学习和使用；采用形式化开发方法会延误项目开发周期、增加开发费用；许多流行的形式化方法对于较小规模项目是有效的，但却很难应用于一些大型系统；形式化方法不能确保开发出完全正确的软件；缺乏对软件生命周期内各个阶段提供全面支持的形式化方法等。,-52-,形式化方法争议,形式化方法中的抽象数学符号及理论确实对软件工程师的使用带来一些不便，以致于人们要花一定的时间和精力去学习和掌握。但是，采用形式化方法可以极大地减少了系统设计开发早期阶段的错误，避免了后期错误修改所带来的高额成本开销，这样早期人员培训的成本开销会在后期的系统测试和维护中的高额回报中得到补偿，在某种程度上还降低了软件开发的成本。同时，采用形式化方法还会提高系统的设计开发效率，并且形式化方法是高质量、高可靠软件开发的有效途径，是软件自动化的根本前提。尽管如此，形式化方法不会完全代替传统的软件开发方法和面向对象方法，软件工程师们需要根据所解决问题的特点结合或选择使用。,-53-,应用形式化方法考虑的因素,应用的类型 形式化方法不可能对所有的应用类型都适用，对于一个项目，应该衡量其问题领域的特点、以及模型的复杂性，从而确定是否适于采用形式方法；规模和结构 在将形式化方法用于一个项目之前，还应该评价项目的规模和结构复杂性。形式化方法可有效地使用于中等规模的系统；为了使大型系统能充分受益于所采用的形式化方法，该系统应该具有很好的结构，并能分解成定义良好的构件，从而使其中的关键部分只受形式化方法的控制；类型的选择 在将形式化方法用于一个项目时，必须能清楚地确定其目标。不同的应用目的将对开发过程产生不同的影响，从而影响到对形式化方法类型的选择；形式化级别 对一个系统可能进行非形式化、半形式化、或者高度形式化的描述，从某个给定项目的目标出发，我们先必须确定其应用的关键程度、项目规模、可用的资源、以及对项目合适的形式化程度等，并从这些可能性中做出一个选择；使用范围 一方面我们需要对形式化方法所应用于的开发阶段进行选择，虽然形式方法可使用于开发过程的所有阶段，但通常只是有选择地使用。另一方面，需要对采用形式化方法的构件进行选择，对那些决定安全性的构件不但需要形式化，而且需要高度的形式化；工具 为了足够精确地实施形式化方法，工具的支持是必须的。针对一个项目，需要综合上面的所有因素来选择合适的工具。,-54-,小结,有益基础研究：复合、抽象、重用模型、数学理论组合、数据结构及算法形式化方法和传统方法以及面向对象的方法结合支撑工具的研究 P.Brooks说“没有银弹”摘自人月神话,-55-,