《形式化方法引论》PPT课件

《《形式化方法引论》PPT课件》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、软件开发的形式化方法引论目录单击此处添加标题文字单击此处添加文字内容单击此处添加文字内容单击此处添加文字内容1单击此处添加标题文字单击此处添加文字内容单击此处添加文字内容单击此处添加文字内容2单击此处添加标题文字单击此处添加文字内容单击此处添加文字内容单击此处添加文字内容3单击此处添加标题文字单击此处添加文字内容单击此处添加文字内容单击此处添加文字内容4形式化方法形式化方法(formalmethods)在逻辑科学中是指分析、研究思维形式结构的方法。它能精确地揭示各种逻辑规律,制定相应的逻辑规则,

2、使各种理论体系更加严密。也能正确地训练思维、提高思维的抽象能力。软件工程方法的一种分类软件工程方法可以按照在软件开发中应用数学的严格程度（即形式化程度），进行分类。完全非形式化的方法：指运用图、文本、表格和简单符号等，去建立各种软件模型。其中不使用数学。完全形式化的方法：以具有良好数学基础和数学表示形式的形式化规格语言，建立各种软件模型。完全非形式化的方法的缺陷各种模型中很容易包含具有矛盾、歧义、含糊、不完整的内容。也容易产生抽象程度的混杂。形式化方法的优点形式化方法支持抽象，利于建模形式化方法

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

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

5、格(Specification)和验证(Verification)的方法。因此，形式化方法又分为形式化规格方法和形式化验证方法。形式化规格是通过具有明确数学定义的文法和语义的方法或语言对软件的期望特性或者行为进行的精确、简洁描述。形式化验证是基于已建立的形式化规格，对软件的相关特性进行评价的数学分析和证明。形式化方法的发展软件的形式化开发方法，最早可追溯到20世纪50年代后期对程序设计语言编译技术的研究。出现了形式化说明和验证编译程序的各种方法J.Backus提出BNF描述Algol60语言的语

6、法出现了各种语法分析程序自动生成器以及语法制导的编译方法，使得编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法。形式化方法的发展在20世纪60年代，面对当时出现的软件危机，Floyd、Hoare和Manna等开展的程序正确性证明研究推动了形式化方法的发展，他们试图用数学方法来证明程序的正确性并发展成为了各种程序验证方法，但是受程序规模的限制，这些方法并未达到预期的应用效果。形式化方法的发展20世纪80年代，在硬件设计领域形式化方法的工业应用结果掀起了软件形式化开发方法的学术研究

7、和工业应用的热潮。Pnueh提出了反应式系统规格和验证的时态逻辑（TemporalLogic，TL）方法。Clarke和Emerson提出了有穷状态并发系统的模型检验(ModelChecking)方法。形式化方法的发展经过几十年的研究和应用，形式化方法取得了大量、重要的成果从早期最简单的形式化方法——一阶谓词演算方法到现在的应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程代数、代数等众多形式化方法形式化方法逐渐融入软件开发过程的各个阶段,从需求分析、功能描述(规约)、(体系结构/算法)设计

8、、编程、测试直至维护。形式化方法的发展近年来，形式化方法的研究及其在工业中的应用得到了长足的发展。研究人员建立了系统设计人员易于理解的规格概念和术语，以及有效应用这些术语和概念的形式化规格方法及语言，建立了功能更加强大和完善的模型检验和定理证明技术。开发出了与之相应的从研究原型到商品化产品的支撑工具和环境。将形式化方法用于软件开发的主要目的是保证软件的正确性。形式化方法基于严格的数学，而在软件开发过程中使用数学具有如下优点：数学是准确的建模媒体，能够对现象、对象、动作等进行简洁、准确地描述。数学