软件工程导论class5形式化说明技术

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

1、软件工程导论第5课第4章形式化说明技术第4章形式化说明技术软件工程方法分类非形式化自然语言半形式化数据流图实体-联系图建立模型形式化有穷状态机Petri网Z语言形式化方法:描述系统性质的基于数学的技术4.1概述4.1.1非形式化方法的缺点矛盾：指一组相互冲突的陈述二义性：读者可以用不同方式理解的陈述含糊性：系统规格说明书是很庞大的文档,难以杜绝含糊性措辞不完整性：对实体的描述不全面抽象层次混乱：在非常抽象的陈述中混进了一些关于细节的低层次陈述4.1.2形式化方法的优点理想的建模工具数学最有用的一个性质是

2、，它能够简洁准确地描述物理现象、对象或动作的结果。特别适于表示状态。在理想情况下，分析员可以写出系统的数学规格说明，它准确到几乎没有二义性，而且可以用数学方法来验证，以发现存在的矛盾和不完整性，在这样的规格说明中完全没有含糊性4.1.2形式化方法的优点可以在不同的软件工程活动之间平滑地过渡不仅功能规格说明，而且系统设计也可以用数学表达提供了高层确认的手段可以使用数学方法证明，设计符合规格说明，程序代码正确地实现了设计结果4.1.3应用形式化方法的准则形式化方法有争议，要一分为二应用形式化方法的准则如下：(1

3、)应该选用适当的表示方法。一种规格说明技术只能用自然的方式说明某一类概念，适用于一定范围(2)应该形式化，但不要过分形式化。目前的形式化技术还不适于描述系统的每个方面。主要用形式化方法仔细说明系统中易出错的或关键的部分4.1.3应用形式化方法的准则(3)应该估算成本为了使用形式化方法，通常需要事先进行大量的培训(4)应该有形式化方法顾问随时提供咨询绝大多数软件工程师对形式化方法中使用的数学和逻辑并不很熟悉，而且没受过使用形式化方法的专业训练需要专家指导和培训4.1.3应用形式化方法的准则(5)不应该放弃传统

4、的开发方法形式化方法和结构化方法或面向对象方法集成起来可能取长补短(6)应该建立详尽的文档使用自然语言注释形式化的规格说明书，以帮助用户和维护人员理解系统4.1.3应用形式化方法的准则(7)不应该放弃质量标准形式化方法仅仅有助于开发出高质量软件的一种手段,系统开发过程中仍然必须一如既往地实施其他质量保证活动(8)不应该盲目依赖形式化方法形式化方法并不能保证开发出的软件绝对正确,，必须用其他方法(例如，评审、测试)来验证软件正确性4.1.3应用形式化方法的准则(9)应该测试、测试再测试形式化方法不仅不能保证软

5、件系统绝对正确，也不能证明系统性能或其他质量指标符合需要，因此，软件测试的重要性并没有降低。(10)应该重用软件重用仍然是降低软件成本和提高软件质量的惟一合理的方法。形式化方法说明的软件构件具有清晰定义的功能和接口，使得它们有更好的可重用性4.2有穷状态机有穷状态机可以准确地描述一个系统，是表达规格说明的一种形式化方法。[保险箱实例]一个保险箱上装了一个复合锁，锁有三个位置，分别标记为1、2、3，转盘可向左(L)或向右(R)转动。这样，在任意时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L和3R。

6、保险箱的组合密码是1L、3R、2L，转盘的任何其他运动都将引起报警。图4.1描绘了保险箱的状态转换情况。4.2.1概念4.2.1概念4.2.1概念有穷状态机5部分状态集J输入集K转换函数T:由当前状态和当前输入确定下一个状态(次态)初始态S终态集F4.2.1概念有穷状态机可以表示为一个5元组(J，K，T，S，F)J是一个有穷的非空状态集；K是一个有穷的非空输入集；T是一个从(J-F)×K到J的转换函数；S∈J，是一个初始状态；F∈J，是终态集。4.2.1概念[保险箱实例]状态集J：｛保险箱锁定，A，B，保

7、险箱解锁，报警｝输入集K：｛1L，1R，2L，2R，3L，3R｝转换函数T：如表4.1所示初始态S：保险箱锁定终态集F：｛保险箱解锁，报警｝4.2.1概念有穷状态机的应用每个菜单驱动的用户界面:一个菜单的显示和一个状态相对应，键盘输入或用鼠标选择一个图标是使系统进入其他状态的一个事件状态的每个转换都具有下面的形式：当前状态〔菜单〕+事件〔所选择的项〕→下个状态。当前状态〔菜单〕+事件〔所选择的项〕+谓词→下个状态增加一个谓词集P，把有穷状态机扩展为一个6元组(J，K，T，S，F，P)4.2.2例子用自然语言

8、描述的电梯系统需求4.2.2例子用有穷状态机描述的电梯系统需求4.2.2例子用有穷状态机描述的电梯系统需求4.2.2例子用有穷状态机描述的电梯系统需求4.2.2例子用有穷状态机描述的电梯系统需求4.2.2例子用有穷状态机描述的电梯系统需求4.2.2例子用有穷状态机描述的电梯系统需求4.2.2例子用有穷状态机描述的电梯系统需求4.2.3评价有穷状态机用简单的格式来描述规格说明4.3Petri网Petri网(Carl