软件工程 - 51testing.ppt

计算机辅助软件工程 实现软件生命周期各个环节的自动化 整个生命周期的支持，解决生产效率 软件工程经济学 从经济学的观点来研究、分析如何有效地开发、发布软件产品和支持用户使用 成本估算技术、模型、效益分析、多目标决策、不确定性的处理、风险分析、工期估计 -*- 1.4 形式化方法 形式化方法概念 发展 目的 形式化方法软件开发— 变换模型 形式化规格 形式化验证 程序求精 形式化方法的应用 -*- 形式化方法概念 形式化方法是渗透在软件生命期中各个环节（如：需求、设计、实现、测试等）的数学方法 或者 具有严格数学基础的软件开发方法 形式化方法的基本含义是借助数学的方法来研究计算机科学中的有关问题。 《Encyclopedia of Software Engineering》对形式化方法定义为：“用于开发计算机系统的形式化方法是基于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框架，人们可以在该框架中以系统的方式刻画、开发和验证系统”。 -*- 形式化方法概念 在软件开发的全过程中，凡是采用严格的数学语言，具有精确的数学语义的方法，都称为形式化方法。 从广义角度，形式化方法是软件开发过程中分析、设计及实现的系统工程方法。 狭义地，形式化方法是软件规格（specification）和验证（verification）的方法。 形式化方法又分为形式化规格方法和形式化验证方法。 形式化规格是通过具有明确数学定义的文法和语义的方法或语言对软件的期望特性或者行为进行的精确、简洁描述。 形式化验证是基于已建立的形式化规格，对软件的相关特性进行评价的数学分析和证明。 -*- 发展历史 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)方法； 近十年来，建立了易于理解的规格概念和术语、形式化规格方法及语言、形式化验证技术:模型检测和定理证明，开发了支撑工具和环境 -*- 形式化方法主要目标 形式化方法用于软件开发的主要目的是保证软件的正确性。 形式化方法基于严格的数学，而在软件开发过程中使用数学具有如下优点：数学是准确的建模媒体，能够对现象、对象、动作等进行简洁、准确的描述；数学支持抽象，它使得规格的本质可以被展示出来，并且还可以以一种有组织的方式来表示系统规格中的抽象层次；数学提供了高层确认的手段，可以使用数学证明来揭示规格中的矛盾性和不完整性、以及用来展示设计和规格之间的一致情况等。 （从软件工程知识体角度）2004年5月，IEEE-CS和ACM联合任务组提交了CCSE（Computing Curriculum-Software Engineering）最终报告，在该报告给出的SEEK（Software Engineering Education Knowledge）中，“软件的形式化方法（Formal Methods in Software Engineering）”被单列为一门必修课程（序列号为SE313）。 -*- 形式化方法软件开发 变化模型：把现实世界的需求反映成软件的模型化过程 模型化涉及：现实世界、模型表示、计算机系统 开发过程的任务分为：模型获取、模型验证、模型变换 模型获取：从现实世界向模型表示转换，对应软件生命周期中的需求分析、规格、设计活动 模型验证：是否满足需求及具有所期望的特性 模型变换：从模型表示向计算机系统变换的过程。关键任务是一致性测试，对应软件生命周期中的实现和测试 这些任务对应三方面的活动：形式化规格、形式化验证、程序求精 -*- （1）形式化规格 软件规格是指对软件系统对象及用来对系统对象进行操作的方法集合，以及对所开发系统中的各对象在其生存期间里的集体行为的描述。软件生命周期模型将整个软件开发过程分解为一系列的阶段，并为每个阶段赋予明确的任务。 “规格”应当理解为一个多阶段的、而不是仅仅某一个阶段的行为。 -*- 需求分析 系统设计I 程序开发 软件测试 软件运行 BS codes PS DS 系统设计II （1）形式