软件工程第4章(不讲).ppt
第第第第4 4章章章章 形式化说明技术形式化说明技术形式化说明技术形式化说明技术4.1 4.1 概述概述概述概述4.2 4.2 有穷状态机有穷状态机有穷状态机有穷状态机4.3 Petri4.3 Petri网网网网4.4 Z4.4 Z语言语言语言语言4.5 4.5 小结小结小结小结形式化方法形式化方法n是描述系统性质的基于是描述系统性质的基于数学数学的技术，有的技术，有坚实的数学基础。坚实的数学基础。n按照形式化的程度，划分成非形式化、按照形式化的程度，划分成非形式化、半形式化和形式化半形式化和形式化3类。类。u用自然语言描述需求规格说明，是典型的用自然语言描述需求规格说明，是典型的非形式化方法。非形式化方法。u用数据流图或实体用数据流图或实体-联系图建立模型，是典联系图建立模型，是典型的半形式化方法。型的半形式化方法。24.1.1 非形式化方法的缺点非形式化方法的缺点n自然语言书写的规格说明书，可能存在自然语言书写的规格说明书，可能存在u矛盾矛盾矛盾矛盾u二义性二义性二义性二义性u含糊性含糊性含糊性含糊性u不完整性不完整性不完整性不完整性u抽象层次混乱抽象层次混乱抽象层次混乱抽象层次混乱34.1.2 形式化方法的优点形式化方法的优点n简洁准确简洁准确简洁准确简洁准确，是理想的建模工具，是理想的建模工具n验证需求，以验证需求，以发现存在的矛盾和不完整性发现存在的矛盾和不完整性发现存在的矛盾和不完整性发现存在的矛盾和不完整性n平滑过渡，也可以用于设计平滑过渡，也可以用于设计n提供了高层提供了高层确认确认的手段的手段u证明设计符合规格说明证明设计符合规格说明u证明程序代码正确地实现了设计结果证明程序代码正确地实现了设计结果44.1.3 应用形式化方法的准则应用形式化方法的准则(1)应该选用适当的表示方法。应该选用适当的表示方法。(2)应该形式化，但不要过分形式化。应该形式化，但不要过分形式化。(3)应该估算成本。应该估算成本。(4)应该有形式化方法顾问随时提供咨询。应该有形式化方法顾问随时提供咨询。(5)不应该放弃传统的开发方法。不应该放弃传统的开发方法。(6)应该建立详尽的文档。应该建立详尽的文档。(7)不应该放弃质量标准。不应该放弃质量标准。(8)不应该盲目依赖形式化方法。不应该盲目依赖形式化方法。(9)应该测试、测试再测试。应该测试、测试再测试。(10)应该重用。应该重用。54.2 有穷状态机有穷状态机例如,当有多个申请占用CPU运行的进程时,有关CPU分配的进程的状态迁移。6进程的状态迁移进程的状态迁移7保险箱的状态转换图保险箱的状态转换图例：一个保险箱上装了一个复合锁，锁例：一个保险箱上装了一个复合锁，锁有三个位置，分别标记为有三个位置，分别标记为1、2、3，转，转盘可向左盘可向左(L)或向右或向右(R)转动。这样，在转动。这样，在任意时刻转盘都有任意时刻转盘都有6种可能的运动，即种可能的运动，即1L、1R、2L、2R、3L和和3R。保险箱的。保险箱的组合密码是组合密码是1L、3R、2L，转盘的任何其，转盘的任何其他运动都将引起报警。他运动都将引起报警。8保险箱的状态转换图保险箱的状态转换图9有穷状态机的状态转换表有穷状态机的状态转换表10有穷状态机的表示有穷状态机的表示n包括包括5个部分：个部分：状态集状态集J、输入集输入集K、由当前状态、由当前状态和当前输入确定下一个状态和当前输入确定下一个状态(次态次态)的的转换函数转换函数T、初始态初始态S和和终态集终态集F。n保险箱的有穷状态机：保险箱的有穷状态机：状态集状态集J：保险箱锁定，：保险箱锁定，A，B，保险箱解锁，报警。，保险箱解锁，报警。输入集输入集K：1L，1R，2L，2R，3L，3R。转换函数转换函数T：如表：如表4.1所示。所示。初始态初始态S：保险箱锁定。：保险箱锁定。终态集终态集F：保险箱解锁，报警。：保险箱解锁，报警。11有穷状态机有穷状态机5元组表示元组表示n表示为一个表示为一个5元组元组(J，K，T，S，F)，其中：其中：J是一个有穷的非空状态集；是一个有穷的非空状态集；K是一个有穷的非空输入集；是一个有穷的非空输入集；T是一个从是一个从(J-F)K到到J的转换函数；的转换函数；SJ，是一个初始状态；，是一个初始状态；FJ，是终态集。，是终态集。12状态转换表示形式状态转换表示形式n状态的每个转换都具有下面的形式：状态的每个转换都具有下面的形式：当前状态当前状态菜单菜单+事件事件所选择的项所选择的项下下个状态。个状态。n加入加入谓词集谓词集P把有穷状态机扩展为一个把有穷状态机扩展为一个6元组，元组，其中每个谓词都是系统全局状态其中每个谓词都是系统全局状态Y的函数。转的函数。转换函数换函数T则是一个从则是一个从(J-F)KP到到J的函数。的函数。转换规则形式如下：转换规则形式如下：当前状态当前状态菜单菜单+事件事件所选择的项所选择的项+谓词谓词下个状态。下个状态。134.3 Petri网网n用于确定并发系统中隐含的定时问题用于确定并发系统中隐含的定时问题nPetri网包含网包含4种元素，四元组种元素，四元组C=(P,T,I,O)u一组位置一组位置PP1，P2，P3，P4u一组转换一组转换Tt1，t2u输入函数输入函数I：I(t1)=P2，P4、I(t2)=P2u输出函数输出函数O：O(t1)=P1、O(t2)=P3，P328Petri网的权标网的权标n在在Petri网中权标网中权标(token)的分配的分配n权标可以用向量权标可以用向量(1，2，0，1)表示表示n当每个输入位置所当每个输入位置所拥有的权标数大于等于从拥有的权标数大于等于从该位置到转换的线数该位置到转换的线数时，就允许转换时，就允许转换nPetri网中权标总数网中权标总数不是固定不是固定的的n带有标记的带有标记的Petri网成为一个五元组网成为一个五元组(P，T，I，O，M)29Petri网网的的转转换换303132 处理两个进程的同步问题3334含禁止线的含禁止线的Petri网网n禁止线是用一个小圆圈而不是用箭头标记的输禁止线是用一个小圆圈而不是用箭头标记的输入线。入线。n通常，当每个输入线上至少有一个权标，而禁通常，当每个输入线上至少有一个权标，而禁止线上没有权标的时候，相应的转换才是允许止线上没有权标的时候，相应的转换才是允许的。的。35
