软件工程导论第4章 形式化说明技术.pptVIP

软件工程导论（第5版） 第4章 形式化说明技术 主要内容 4.1 形式化说明技术 4.2 有穷状态机 4.3 Petri网 4.4 Z语言 教学重点 有穷状态机、 Petri网。 4.1形式化说明技术概述 形式化方法的引入 在传统的软件开发过程中，人们普遍采用各种非形式化的图形工具和文字符号工具，并按照一定的设计原则和有序步骤，同时手工或辅助编写有关设计文档。 软件工程的实践表明，用户需求规格说明的质量对于后续的软件开发过程是非常重要的。 系统分析人员依据用户需求，为目标软件系统创建了需求规格说明。 设计和编程人员根据这个需求规格说明进行系统结构和模块设计及编码。 软件测试及验收人员则根据这个需求规格说明验证目标系统。 4.1 续 形式化方法的引入 20世纪80年代中期以来，一种专用于需求规格说明的形式规格说明语言应运而生。 形式规格说明语言克服了自然语言和程序设计语言的不足，应用形式化、规范化的数学理论，严格定义软件系统“做什么”的形式语义模型，并支持自动程序转换系统将需求规格说明的语义模型转换为可执行代码。由此产生的软件形式开发方法正日益受到各国软件界的重视。 4.1 续 软件需求规格说明方法分类 非形式化方法 用自然语言进行描述的方式。 半形式化方法 用数据流图、实体-联系图、状态转换图、IPO图等建立模型的方法。 形式化方法 利用形式化、规范化的数学推演的方式。 4.1 续 非形式化方法的缺点 矛盾 一组相互冲突的陈述。 二义性 读者可以用不同方式理解的陈述。 含糊性 没有给出任何有用信息的笼统的陈述。 不完整性 信息的描述过程中遗留了某个方面。 抽象层次混乱 在非常抽象的陈述中混进了一些关于细节的低层陈述。 4.1 续 形式化方法的主要思想 形式化需求分析方法的主要思想，是利用形式化规格说明语言严格地定义用户需求，并采用数学推演的方法证明需求定义的性质。 从某种意义上讲，形式化方法是克服需求分析阶段中主要困难（不精确性、不一致性和不完全性）的有效途径。 形式化规格说明语言包括：严格的语法定义、严格的语义定义以及一系列的数学推演规则。 4.1 续 形式化方法的主要思想 规格说明语言的语法一般基于集合论、数理逻辑或代数学。 规格说明语言的语义是其所有语法符号的意义的数学描述。 形式化规格说明语言的推演规则一般与其数学基础和语义定义方法密切相关。 规则必须在规格说明语言的语义系统中可证。因此，可以认为规则是派生的语义定义，它们可以直接应用于软件规格说明的性质证明并简化推演过程。 4.1 续 形式化方法的分类 形式化方法是应用严格的形式符号和数学方法定义或描述目标软件系统需求规格说明的一种方法。 根据对需求规格说明的定义方式分类： ⒈面向模型的形式方法。 又称基于状态描述的形式方法。 基本思想：利用域、元组、集合、序列、映射、包等这些已知特性的数学抽象概念来为目标软件系统的状态特征和行为特征构造形式语义模型。语义模型就作为目标软件系统需求规格的形式说明。 主要代表：VDM方法（维也纳开发方法）、Z语言方法等。 ⒉代数构造形式方法。 目标软件系统的需求规格说明提供一些特殊的构造机制，并以代数构造方式描述目标系统的结构、功能。 4.1 续 软件形式开发方法 将形式化方法应用于软件开发过程称为软件形式开发方法。 首先，在需求分析阶段的信息收集和信息分析两项工作中，采用形式化的规格说明语言构造目标软件系统严格的形式需求规格说明即形式语义。 然后，以该形式需求规格说明为起点，借助相应的形式开发支持工具辅助实现目标软件系统。 目前，除了在软件设计、编码阶段采用形式方法外，还在开展软件系统形式化测试的研究工作。 4.1 续 形式化方法的优点 ⒈对系统的需求规格说明描述精确、定义完整。 ⒉形式化的需求规格说明有利于系统的设计与实现。 ⒊软件实现的正确性可以形式验证，确保软件质量。 4.1 续 形式化方法的缺点 ⒈形式化的需求规格说明可读性差。 ⒉对软件设计人员要求较高，需进行更专业化的培训。 ⒊只适用于能静态定义的软件系统，它无法定义动态系统行为。 ⒋形式化的规格说明（形式语义模型）的正确性验证费时费力，目前还不能简化或自动化。 ⒌形式方法目前还缺乏软件工程环境的支持。 4.1 续 应用形式化方法的准则 ⑴应该选用适合当前项目的形式化说明技术。 ⑵应该形式化，但不要过分形式化。 ⑶应该估算成本。 ⑷应该有形式化方法顾问随时提供咨询。 ⑸不应该放弃传统的开发方法。 ⑹应该建立详尽的文档。 ⑺不应该放弃质量标准。 ⑻不应该盲目依赖形式化方法。 ⑼应该进行严格的审查、验证。 ⑽应该重用。 4.1 续 形式化方法近年来的发展 ⒈形式化方法与图形语言机制相结合。为图形语言机制赋予形式化的语法和语义，从而兼具了图形表示的直观、简洁，以及形