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

《软件工程导论第4章形式化说明技术》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、软件工程导论（第5版）普通高校本科计算机专业特色教材精选张海藩编著第4章形式化说明技术主要内容4.1形式化说明技术4.2有穷状态机4.3Petri网4.4Z语言教学重点有穷状态机、Petri网。4.1形式化说明技术概述形式化方法的引入在传统的软件开发过程中，人们普遍采用各种非形式化的图形工具和文字符号工具，并按照一定的设计原则和有序步骤，同时手工或辅助编写有关设计文档。软件工程的实践表明，用户需求规格说明的质量对于后续的软件开发过程是非常重要的。系统分析人员依据用户需求，为目标软件系统创建了需求规格说明。设计和编程人员根据这个需求规格说明进行系统结构和模块设计及编码。软件测试及验收人员则根据

2、这个需求规格说明验证目标系统。4.1续形式化方法的引入20世纪80年代中期以来，一种专用于需求规格说明的形式规格说明语言应运而生。形式规格说明语言克服了自然语言和程序设计语言的不足，应用形式化、规范化的数学理论，严格定义软件系统“做什么”的形式语义模型，并支持自动程序转换系统将需求规格说明的语义模型转换为可执行代码。由此产生的软件形式开发方法正日益受到各国软件界的重视。4.1续软件需求规格说明方法分类非形式化方法用自然语言进行描述的方式。半形式化方法用数据流图、实体-联系图、状态转换图、IPO图等建立模型的方法。形式化方法利用形式化、规范化的数学推演的方式。4.1续非形式化方法的缺点矛盾一组相

3、互冲突的陈述。二义性读者可以用不同方式理解的陈述。含糊性没有给出任何有用信息的笼统的陈述。不完整性信息的描述过程中遗留了某个方面。抽象层次混乱在非常抽象的陈述中混进了一些关于细节的低层陈述。4.1续形式化方法的主要思想形式化需求分析方法的主要思想，是利用形式化规格说明语言严格地定义用户需求，并采用数学推演的方法证明需求定义的性质。从某种意义上讲，形式化方法是克服需求分析阶段中主要困难（不精确性、不一致性和不完全性）的有效途径。形式化规格说明语言包括：严格的语法定义、严格的语义定义以及一系列的数学推演规则。4.1续形式化方法的主要思想规格说明语言的语法一般基于集合论、数理逻辑或代数学。规格说明语

4、言的语义是其所有语法符号的意义的数学描述。形式化规格说明语言的推演规则一般与其数学基础和语义定义方法密切相关。规则必须在规格说明语言的语义系统中可证。因此，可以认为规则是派生的语义定义，它们可以直接应用于软件规格说明的性质证明并简化推演过程。4.1续形式化方法的分类形式化方法是应用严格的形式符号和数学方法定义或描述目标软件系统需求规格说明的一种方法。根据对需求规格说明的定义方式分类：⒈面向模型的形式方法。又称基于状态描述的形式方法。基本思想：利用域、元组、集合、序列、映射、包等这些已知特性的数学抽象概念来为目标软件系统的状态特征和行为特征构造形式语义模型。语义模型就作为目标软件系统需求规格的形

5、式说明。主要代表：VDM方法（维也纳开发方法）、Z语言方法等。⒉代数构造形式方法。目标软件系统的需求规格说明提供一些特殊的构造机制，并以代数构造方式描述目标系统的结构、功能。4.1续软件形式开发方法将形式化方法应用于软件开发过程称为软件形式开发方法。首先，在需求分析阶段的信息收集和信息分析两项工作中，采用形式化的规格说明语言构造目标软件系统严格的形式需求规格说明即形式语义。然后，以该形式需求规格说明为起点，借助相应的形式开发支持工具辅助实现目标软件系统。目前，除了在软件设计、编码阶段采用形式方法外，还在开展软件系统形式化测试的研究工作。4.1续形式化方法的优点⒈对系统的需求规格说明描述精确、定

6、义完整。⒉形式化的需求规格说明有利于系统的设计与实现。⒊软件实现的正确性可以形式验证，确保软件质量。4.1续形式化方法的缺点⒈形式化的需求规格说明可读性差。⒉对软件设计人员要求较高，需进行更专业化的培训。⒊只适用于能静态定义的软件系统，它无法定义动态系统行为。⒋形式化的规格说明（形式语义模型）的正确性验证费时费力，目前还不能简化或自动化。⒌形式方法目前还缺乏软件工程环境的支持。4.1续应用形式化方法的准则⑴应该选用适合当前项目的形式化说明技术。⑵应该形式化，但不要过分形式化。⑶应该估算成本。⑷应该有形式化方法顾问随时提供咨询。⑸不应该放弃传统的开发方法。⑹应该建立详尽的文档。⑺不应该放弃质量标

7、准。⑻不应该盲目依赖形式化方法。⑼应该进行严格的审查、验证。⑽应该重用。4.1续形式化方法近年来的发展⒈形式化方法与图形语言机制相结合。为图形语言机制赋予形式化的语法和语义，从而兼具了图形表示的直观、简洁，以及形式化方法的严谨、精确等优点。⒉用CASE工具支持形式化软件开发。CASE工具不仅可以简化需求分析和需求描述工作，而且还可以利用自动定理证明技术帮助分析人员验证软件规格说明的数学性质。实践证