第4章 形式化说明技术.pptVIP

软 件 工 程 第4章 形式化说明技术 4.1 概述 4.2 有穷状态机 4.3 Petri网 4.4 Z语言 4.5 小结 按照形式化的程度，可以把软件工程使用的方法划分成非形式化、半形式化和形式化3类。 其中：用自然语言描述需求规格说明，是典型的非形式化方法。用数据流图或实体-联系图建立模型，是典型的半形式化方法。 【定义】：用数学工具描述现实业务系统发生的各种活动。 §4.1 概述 §4.1.1 非形式化方法的缺点 用自然语言书写的系统规格说明书，可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。 所谓矛盾是指一组相互冲突的陈述。 二义性是指读者可以用不同方式理解的陈述。 §4.1.2 形式化方法的优点 为了克服非形式化方法用自然语言描述的规格说明时的缺点(二义性)，人们把数学引入软件开发过程，创造了基于数学的形式化方法。 在开发大型软件系统的过程中应用数学，能够带来下述的几个优点： 【优点1】：数学最有用的一个性质是，它能够简洁准确地描述物理现象、对象或动作的结果，因此是理想的建模工具。数学特别适合于表示状态，也就是表示“做什么”。 【优点2】：可以在不同的软件工程活动之间平滑地过渡。不仅是功能规格说明，而且系统设计也可以用数学表达，当然，程序代码本身就是一种数学符号。 【优点3】：它提供了高层确认的手段。可以使用数学方法证明，设计符合规格说明，程序代码正确地实现了设计结果。 §4.1.3 应用形式化方法的准则 人们对形式化方法的看法并不一致，由拥护者，也有反对者，尤其是对开发周期短的管理信息系统(MIS)来说应慎用形式化方法去验证需求内容，用户很反感。 具体使用时，根据所编写的软件类型和规模要有所区分，即不要过分夸大它的优点也不要一概排斥。 为了更好地发挥这种方法的长处，下面解释几条应用形式化方法的准则，供学生们在以后的实际工作中使用。 (1)选择适用于当前项目的符号系统。 (2) 应该形式化，但不要过分形式化。 (3) 应该进行成本/效益分析。为了使用形式化方法，通常需要事先进行大量的培训。 (4) 应该有形式化方法顾问随时提供咨询。绝大多数软件工程师没受过使用形式化方法的专业训练。 (5) 不应该放弃传统的开发方法。把形式化方法和结构化方法或面向对象方法集成起来用，可取得很好的效果。 (6) 应该建立详尽的文档。以帮助用户和维护人员理解系统。 (7) 不应该放弃质量标准。形式化方法并不能保证软件的正确性，它们只不过是有助于开发出高质量软件的一种手段。 (8) 不应该盲目依赖形式化方法。它是众多工具中的一种。形式化方法并不能保证开发出的软件绝对正确。 (9) 应该测试、测试再测试。形式化方法不仅不能保证软件系统绝对正确，也不能证明系统性能或其他质量指标符合需要。所以测试非常重要。 (10) 应该重用。即使采用了形式化方法，软件重用仍然是降低软件成本和提高软件质量的唯一合理的方法。例如：用形式化方法说明的软件构件具有清晰定义的功能和接口，使得它们具有更好的可重用性。 §4.2 有穷状态机 利用有穷状态机可以准确地描述一个系统，因此它是表达规格说明的一种形式化方法。 【应用举例】：有穷状态机的概念在计算机系统中应用得非常广泛。例如，每个菜单驱动的用户界面都是一个有穷状态机的实现。一个菜单的显示和一个状态相对应，键盘输入或用鼠标选择一个图标是使系统进入其他状态的一个事件。状态的每个转换都具有下面的形式： 当前状态〔菜单〕+事件〔所选择的项〕下个状态。 §4.3 Petri网 并发系统中遇到的一个主要问题是定时问题。这个问题可以表现为多种形式，如同步问题、竞争条件以及死锁问题。 用于确定系统中隐含的定时问题的一种有效技术是Petri网，这种技术的一个很大的优点是它也可以用于设计中。 最初只有自动化专家对Petri网感兴趣，后来Petri网在计算机科学中也得到广泛的应用。 例如，在性能评价、操作系统和软件工程等领域，Petri网应用得都比较广泛。特别是已经证明，用Petri网可以有效地描述并发活动，在很多领域中得到应用，例如信息安全中的安全性的验证。 Petri网包含4种元素：一组位置P、一组转换T、输入函数I以及输出函数O。 具体应用的案例可参考课本中的电梯Petri网。如图所示是一个基于PKI身份认证系统认证协议的安全性分析Petri网： §4.4 Z语言 具备的知识： 集合论、函数、数理逻辑 主要是通过研究生阶段的学习才能掌握Z语言。 使用形式化规格说明是全球的总趋势。主要是欧洲习惯于使用形式化规格说明技术，现在越来越多的美国公司也开始使用形式化规格说明技术。 国内还很少见。 §4.5 小结 形式化方法比非形式化方法更难学习，不仅在培训阶段要花大量的