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

软件工程导论第5课第4章形式化说明技术第4章形式化说明技术软件工程方法分类非形式化自然语言半形式化数据流图实体-联系图建立模型形式化有穷状态机Petri网Z语言形式化方法:描述系统性质的基于数学的技术4.1概述4.1.1非形式化方法的缺点矛盾：指一组相互冲突的陈述二义性：读者可以用不同方式理解的陈述含糊性：系统规格说明书是很庞大的文档,难以杜绝含糊性措辞不完整性：对实体的描述不全面抽象层次混乱：在非常抽象的陈述中混进了一些关于细节的低层次陈述4.1.2形式化方法的优点理想的建模工具数学最有用的一个性质是，它能够简洁准确地描述物理现象、对象或动作的结果。特别适于表示状态。在理想情况下，分析员可以写出系统的数学规格说明，它准确到几乎没有二义性，而且可以用数学方法来验证，以发现存在的矛盾和不完整性，在这样的规格说明中完全没有含糊性4.1.2形式化方法的优点可以在不同的软件工程活动之间平滑地过渡不仅功能规格说明，而且系统设计也可以用数学表达提供了高层确认的手段可以使用数学方法证明，设计符合规格说明，程序代码正确地实现了设计结果4.1.3应用形式化方法的准则形式化方法有争议，要一分为二应用形式化方法的准则如下：(1)应该选用适当的表示方法。一种规格说明技术只能用自然的方式说明某一类概念，适用于一定范围(2)应该形式化，但不要过分形式化。目前的形式化技术还不适于描述系统的每个方面。主要用形式化方法仔细说明系统中易出错的或关键的部分4.1.3应用形式化方法的准则(3)应该估算成本为了使用形式化方法，通常需要事先进行大量的培训(4)应该有形式化方法顾问随时提供咨询绝大多数软件工程师对形式化方法中使用的数学和逻辑并不很熟悉，而且没受过使用形式化方法的专业训练需要专家指导和培训4.1.3应用形式化方法的准则(5)不应该放弃传统的开发方法形式化方法和结构化方法或面向对象方法集成起来可能取长补短(6)应该建立详尽的文档使用自然语言注释形式化的规格说明书，以帮助用户和维护人员理解系统4.1.3应用形式化方法的准则(7)不应该放弃质量标准形式化方法仅仅有助于开发出高质量软件的一种手段,系统开发过程中仍然必须一如既往地实施其他质量保证活动(8)不应该盲目依赖形式化方法形式化方法并不能保证开发出的软件绝对正确,，必须用其他方法(例如，评审、测试)来验证软件正确性4.1.3应用形式化方法的准则(9)应该测试、测试再测试形式化方法不仅不能保证软件系统绝对正确，也不能证明系统性能或其他质量指标符合需要，因此，软件测试的重要性并没有降低。(10)应该重用软件重用仍然是降低软件成本和提高软件质量的惟一合理的方法。形式化方法说明的软件构件具有清晰定义的功能和接口，使得它们有更好的可重用性4.2有穷状态机有穷状态机可以准确地描述一个系统，是表达规格说明的一种形式化方法。[保险箱实例]一个保险箱上装了一个复合锁，锁有三个位置，分别标记为1、2、3，转盘可向左(L)或向右(R)转动。这样，在任意时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L和3R。保险箱的组合密码是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，保险箱解锁，报警｝输入集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例子用自然语言描述的电梯系统需求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网(CarlAdamPetri发明)用于确定系统中隐含的定时问题的一种有效技术,用于解决如同步问题、竞争条件以及死锁问题等问题应用领域自动化性能评价操作系统软件工程有效地描述并发活动4.3.1概念Petri4元素一组位置P一组转换T输入函数I输出函数OP为｛P1，P2，P3，P4｝，圆圈T为｛t1，t2｝，短直线I(t1)=｛P2，P4｝I(t2)=｛P2｝,位置指向转换的箭头O(t1)=｛P1｝O(t2)=｛P3，P3｝4.3.1概念形式化的Petri网结构四元组,C=(P,T,I,O)。P=｛P1，…，Pn｝是一个有穷位置集，n≥0。T=｛t1，…，tm｝是一个有穷转换集，m≥0，且T和P不相交。I：T→P∞为输入函数，是由转换到位置无序单位组(bags)的映射。O：T→P∞为输出函数，是由转换到位置无序单位组的映射。无序单位组或多重组是允许一个元素有多个实例的广义集4.3.1概念Petri网的权标·，见图4.6P1中1个小黑点，P2中2个，P4中1个可用向量表示(1，2，0，1)当一个位置拥有的权标数大于等于从它到转换的线数时，就允许转换当t1被激发，P2和P4各有一个权标被移走，P1增加一个权标4.3.1概念图4.7上P2有权标，因此t2也被激发，P2移走一个权标，P3上新增加2个权标，如图4.8所示。形式化说，Petri网是一组位置到一向量的映射M：P→{0,1，2，…}带有标记的Petri网成为一个5元组(P，T，I，O，M)4.3.1概念对Petri网的一个重要扩充是加入禁止线，禁止线用一个小圆圈标记输入线。当输入线上至少有一个权标，而禁止线上没有权标时，相应的转换才是允许的。如图4.9，P3上有一个权标而P2上没有，因此转换t1可以激发。4.3.2例子Ff表示楼层，电梯用权标代表，在位置Ff有权标，表示在楼层f上有电梯。电梯中楼层f的按钮，用位置EBf表示。在EBf上有一个权标，表示电梯内楼层f的按钮被按下了。2楼层按钮4.4Z语言在形式化的规格说明语言中，Z语言贏得了广泛的赞誉。使用Z语言需要具备集合论、函数、数理逻辑等方面的知识。Z语言是相当难学的，因为它除了使用集合论和数理逻辑符号外，还使用一些特殊符号。4.4.1简介用Z语言描述的、最简单的形式化规格说明含有下述4部分给定的集合、数据类型及常数状态定义初始状态操作1给定的集合给定的初始化集合，就是不需要详细定义的集合，用带方括号的形式表示。例如：电梯问题给定的初始化集合称为Button表示：[Button]2状态定义一个Z规格说明由几个格(schema)组成，每个格由一组变量说明和一系列限定变量取值范围的谓词，例如图4.12图4.13是电梯例子的状态定义3初始状态第一次开启时的状态电梯的初始状态表示：当系统首次开启时pushed集为空，即所有的按钮都处于关闭状态。4操作Z语言语法规定，当一个格被用在另一个格中时，要在它的前面加上一个三角形符号电梯的例子△4操作电梯例子，到达楼层△4.4.2评价Z语言成功的原因：(1)容易发现用Z写的规格说明的错误(2)用Z写规格说明时，要十分精确地使用Z说明符，减少了不一致性和遗漏。(3)可以严格地验证说明的正确性。(4)学会编写Z规格说明比较容易(5)减少开发总时间，减少费用(6)可以用自然语言重写规格说明，说明更清楚，更正确。