《形式化说明技术》PPT课件

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

1、软件工程张聚礼zhjl@lut.cn兰州理工大学计算机与通信学院第4章形式化说明技术4.1概述4.2有穷状态机4.3Petri网4.4Z语言4.5小结2按照形式化的程度，可以把软件工程使用的方法划分成非形式化、半形式化和形式化3类。其中：用自然语言描述需求规格说明，是典型的非形式化方法。用数据流图或实体-联系图建立模型，是典型的半形式化方法。【定义】：用数学工具描述现实业务系统发生的各种活动。3§4.1概述§4.1.1非形式化方法的缺点用自然语言书写的系统规格说明书，可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。所谓矛

2、盾是指一组相互冲突的陈述。二义性是指读者可以用不同方式理解的陈述。4§4.1.2形式化方法的优点为了克服非形式化方法用自然语言描述的规格说明时的缺点(二义性)，人们把数学引入软件开发过程，创造了基于数学的形式化方法。在开发大型软件系统的过程中应用数学，能够带来下述的几个优点：【优点1】：数学最有用的一个性质是，它能够简洁准确地描述物理现象、对象或动作的结果，因此是理想的建模工具。数学特别适合于表示状态，也就是表示“做什么”。•5【优点2】：可以在不同的软件工程活动之间平滑地过渡。不仅是功能规格说明，而且系统设计也可以用数学表达，当然

3、，程序代码本身就是一种数学符号。【优点3】：它提供了高层确认的手段。可以使用数学方法证明，设计符合规格说明，程序代码正确地实现了设计结果。6§4.1.3应用形式化方法的准则人们对形式化方法的看法并不一致，由拥护者，也有反对者，尤其是对开发周期短的管理信息系统(MIS)来说应慎用形式化方法去验证需求内容，用户很反感。具体使用时，根据所编写的软件类型和规模要有所区分，即不要过分夸大它的优点也不要一概排斥。为了更好地发挥这种方法的长处，下面解释几条应用形式化方法的准则，供学生们在以后的实际工作中使用。•7(1)选择适用于当前项目的符号系统

4、。(2)应该形式化，但不要过分形式化。(3)应该进行成本/效益分析。为了使用形式化方法，通常需要事先进行大量的培训。(4)应该有形式化方法顾问随时提供咨询。绝大多数软件工程师没受过使用形式化方法的专业训练。•8(5)不应该放弃传统的开发方法。把形式化方法和结构化方法或面向对象方法集成起来用，可取得很好的效果。(6)应该建立详尽的文档。以帮助用户和维护人员理解系统。(7)不应该放弃质量标准。形式化方法并不能保证软件的正确性，它们只不过是有助于开发出高质量软件的一种手段。(8)不应该盲目依赖形式化方法。它是众多工具中的一种。形式化方法并

5、不能保证开发出的软件绝对正确。•9(9)应该测试、测试再测试。形式化方法不仅不能保证软件系统绝对正确，也不能证明系统性能或其他质量指标符合需要。所以测试非常重要。(10)应该重用。即使采用了形式化方法，软件重用仍然是降低软件成本和提高软件质量的唯一合理的方法。例如：用形式化方法说明的软件构件具有清晰定义的功能和接口，使得它们具有更好的可重用性。10§4.2有穷状态机利用有穷状态机可以准确地描述一个系统，因此它是表达规格说明的一种形式化方法。【应用举例】：有穷状态机的概念在计算机系统中应用得非常广泛。例如，每个菜单驱动的用户界面都是一

6、个有穷状态机的实现。一个菜单的显示和一个状态相对应，键盘输入或用鼠标选择一个图标是使系统进入其他状态的一个事件。状态的每个转换都具有下面的形式：当前状态〔菜单〕+事件〔所选择的项〕下个状态。11§4.3Petri网并发系统中遇到的一个主要问题是定时问题。这个问题可以表现为多种形式，如同步问题、竞争条件以及死锁问题。用于确定系统中隐含的定时问题的一种有效技术是Petri网，这种技术的一个很大的优点是它也可以用于设计中。•12最初只有自动化专家对Petri网感兴趣，后来Petri网在计算机科学中也得到广泛的应用。例如，在性能评价、操作

7、系统和软件工程等领域，Petri网应用得都比较广泛。特别是已经证明，用Petri网可以有效地描述并发活动，在很多领域中得到应用，例如信息安全中的安全性的验证。Petri网包含4种元素：一组位置P、一组转换T、输入函数I以及输出函数O。•13具体应用的案例可参考课本中的电梯Petri网。如图所示是一个基于PKI身份认证系统认证协议的安全性分析Petri网：14§4.4Z语言具备的知识：集合论、函数、数理逻辑主要是通过研究生阶段的学习才能掌握Z语言。•15使用形式化规格说明是全球的总趋势。主要是欧洲习惯于使用形式化规格说明技术，现在越来

8、越多的美国公司也开始使用形式化规格说明技术。国内还很少见。16§4.5小结形式化方法比非形式化方法更难学习，不仅在培训阶段要花大量的投资，且对某些软件工程师来说，它代表了一种“文化冲击”，也是今后的使用方向。【应用措施】：把形式化方法