软件工程-第四章

软件工程导论第四章形式化说明技术(FormalDescriptionTechnique，FDT)2019/12/1524.1概述4.2有穷状态机(FSM/FSA)4.3Petri网(PetriNets)4.4Z语言(ZNotation)4.5小结2019/12/1534.1概述按照形式化的程度，可以把软件工程使用的方法划分成非形式化、半形式化和形式化三类非形式化方法(Informal)用自然语言描述需求规格说明半形式化方法(Semi-formal)用数据流图或实体-联系图建立模型形式化方法(Formal)是描述系统性质的基于数学的技术即如果一种方法有坚实的数学基础，那么它就是形式化的2019/12/1544.1概述4.1.1非形式化方法的缺点矛盾：相互冲突的陈述二义性：读者可以用不同的方式理解的陈述含糊：笼统的陈述不完整性：最常遇到的问题抽象层次混乱：非常抽象的陈述中混进了一些关于细节的低层次陈述2019/12/1554.1概述4.1.2形式化方法的优点把数学引入软件开发过程，形成基于数学的形式化方法数学最有用的一个性质是，能够简洁准确地描述物理现象、对象或动作的结果，因此是理想的建模工具。数学特别适合于表示状态，也就是表示“做什么”在理想情况下，分析员可以写出不含二义性的系统的数学规格说明，并可用数学方法对其进行验证，以发现存在的矛盾和不完整性，在这样的规格说明中完全没有含糊性事实上复杂的软件系统通常难以用几个数学公式来描述在软件开发过程中使用数学，可以在不同的软件工程活动之间平滑地过渡（系统规格说明、系统设计、程序代码）提供了高层确认的手段可以使用数学方法证明，设计符合规格说明，程序代码正确地实现了设计结果2019/12/1564.1概述4.1.3应用形式化方法的准则应该选用适当的表示方法，选择适用于当前项目的符号系统应该形式化，但不要过分形式化用形式化方法说明系统中易出错的或关键的部分应该估算成本估算由额外培训所带来的成本并将其编入预算应该有形式化方法顾问随时提供咨询不应该放弃传统的开发方法形式化与SA和OOA结合，取长补短2019/12/1574.1概述4.1.3应用形式化方法的准则应该建立详尽的文档用自然语言注释形式化的规格说明书，以帮助读者理解系统。不应该放弃质量标准形式化方法并不能完全确保软件的正确性，在系统开发过程中必须一如既往地实施其他SQA活动。不应该盲目依赖形式化方法无法用形式化方法证明从非形式化需求到形式化规格说明的转换是正确的，因此，必须用其他方法(例如，评审、测试)来验证软件正确性应该测试、测试再测试由于形式化方法不能保证系统绝对正确，因此，软件测试的重要性并没有降低。应该重用即使使用了形式化方法，软件重用仍然是降低软件成本和提高软件质量的唯一合理的方法。2019/12/1584.2有穷状态机(FSM/FSA)4.2.1概念FSM(Finite-StateMachine)/FSA(Finite-StateAutomaton)isamodelofbehaviorcomposedofafinitenumberofstates,transitionsbetweenthosestates,andactions一个保险箱上装了一个复合锁，锁有3个位置，分别标记为1、2、3，转盘可向左（L）或向右（R）转动这样，任何时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L、3R保险箱的组合密码是1L、3R、2L，转盘的任何其他运动都将引起报警2019/12/1594.2有穷状态机(FSM/FSA)图4.1保险箱的状态转换图statetransitiontransitioncondition2019/12/1510StateTransitionTable2019/12/1511FSM/FSA的数学模型FSM可以表示为一个5元组（J，K，T，S，F）状态集J(finite,non-emptysetofstates)：{保险箱锁定，A，B，保险箱解锁，报警}输入集K(finite,non-emptysetofinput)：{1L、1R、2L、2R、3L、3R}初始态S(initialstate,anelementofJ,i.e.S∈J)：保险箱锁定终态集F(finalstates,a(possiblyempty)subsetofJ,FJ)：{保险箱解锁，报警}转换函数T(state-transitionfunction,(J-F)*KJ)：如表4.1所示2019/12/1512FSM/FSA的数学模型加入谓词集P，把有穷状态机扩展为一个6元组，其中每个谓词都是系统全局状态Y的函数则转换函数T：（J-F）*K*PJ2019/12/1513当前状态〔菜单〕+事件〔所选择的项〕=为了对一个系统进行规格说明，通常都需要对有穷状态机做一个很有用的扩展，即在前述的5元组中加入第6个组件——谓词集P，即把有穷状态机扩展为一个6元组，其中每个谓词都是系统全局状态Y的函数。转换函数T现在是一个从(J-F)×K×P到J的函数。现在的转换规当前状态〔菜单〕+事件〔所选择的项〕+谓词=2019/12/15144.2有穷状态机(FSM/FSA)在一幢m层的大厦中需要一套控制n部电梯的产品，要求这n部电梯按照约束条件C1，C2和C3在楼层间移动C1：每部电梯内有m个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭C2：除了大厦的最低层和最高层之外，每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动C3：当对电梯没有请求时，它关门并停在当前楼层2019/12/15154.2有穷状态机(FSM/FSA)电梯按钮EB（e，f）：按下电梯e内的按钮并请求到f层去状态：EBON（e，f）：电梯按钮（e，f）打开EBOFF（e，f）：电梯按钮（e，f）关闭事件EBP（e，f）：电梯按钮（e，f）被按下EAF（e，f）：电梯到达f层谓词V（e，f）：电梯e停在f层2019/12/1516令EB(e,f)表示按下电梯e内的按钮并请求到f层去。EB(e,f)有两个状态，分别是按钮发光(打开)和不发光(关闭)。更EBON(e,f)：电梯按钮(e，f)EBOFF(e,f)：电梯按钮(e，f)如果电梯按钮(e,f)发光且电梯到达f层，该按钮将熄灭。相反如果按钮熄灭，则按下它时，按钮将发光。上述描述中包含了两个事件，它们分别是：2019/12/1517EBP(e,f)：电梯按钮(e,f)EAF(e,f)：电梯e到达f为了定义与这些事件和状态相联系的状态转换规则，需要一个谓词V，(e,f)V(e,f)：电梯e停在f如果电梯按钮(e,f)处于关闭状态〔当前状态〕，而且电梯按钮(e,f)被按下〔事件〕，而且电梯e不在f层〔谓词〕，则该电梯按钮打开发光〔下个状态〕。状态转换规则的形式化描述如下：EBOFF(e,f)+EBP(e,f)+notV(e,f)=EBON(e,f)反之，如果电梯到达f层，而且电梯按钮是打开的，于是EBON(e,f)+EAF(e,f)=EBOFF(e,f)2019/12/15184.2有穷状态机(FSM/FSA)图4.2电梯按钮的状态转换图EBOFF(e,f)+EBP(e,f)+notV(e,f)EBON(e,f) EBON(e,f)+EAF(e,f)EBOFF(e,f)2019/12/15194.2有穷状态机(FSM/FSA)楼层按钮FB（d，f）：f层请求电梯向d方向运动的按钮状态：FBON（d，f）：楼层按钮（d，f）打开FBOFF（d，f）：楼层按钮（d，f）关闭事件FBP（d，f）：楼层按钮（d，f）被按下EAF（1…n，f）：电梯1或…或n到达f层谓词S（d，e，f）：电梯e停在f层并且移动方向由d确定2019/12/1520接下来让我们考虑楼层按钮。令FB(d,f)表示f层的按钮请求电梯向d方向运动，楼层按钮FB(d,f)的状态转换图如图4.3FBON(d,f)：楼层按钮(d,f)FBOFF(d,f)：楼层按钮(d,f)如果楼层按钮已经打开，而且一部电梯到达f层，则按钮关闭。反之，如果楼层按钮原来是关闭的，被按下后该FBP(d,f)：楼层按钮(d,f)EAF(1··n,f)：电梯1或…或n到达f其中1··n表示或为1或为2…或为n。2019/12/1521为了定义与这些事件和状态相联系的状态转换规则，同样也需要一个谓词，它是S(d,e，f)，它的S(d,e,f)：电梯e停在f层并且移动方向由d确定为向上(d=U)或向下(d=D)或待定(d=N)这个谓词实际上是一个状态，形式化方法允许使用谓词S(d,e,f)FBOFF(d,f)+FBP(d,f)+notS(d,1··n,f)=FBON(d,f)FBON(d,f)+EAF(1··n,f)+S(d,1··n,f)=FBOFF(d,f)其中，d=UorD。2019/12/15224.2有穷状态机(FSM/FSA)FBOFF(d,f)+FBP(d,f)+notS(d,1n,f)FBON(d,f)…FBON(d,f)+EAF(1n,f)+S(d,1n,f)FBOFF(d,f)……图4.3楼层按钮的状态转换图2019/12/1523也就是说，如果在f层请求电梯向d方向运动的楼层按钮处于关闭状态，现在该按钮被按下，并且当时没有正停在f层准备向d方向移动的电梯，则该楼层按钮打开。反之，如果楼层按钮已经打开，且至少有一部电梯到达f层，该部电梯将朝d在讨论电梯按钮状态转换规则时定义的谓词V(e,f)，可以用谓词S(d,e,f)V(e,f)=S(U,e,f)orS(D,e,f)orS(N,e,f)定义电梯按钮和楼层按钮的状态都很简单、直观的事情。现在转向讨论电梯的状态及其转换规则，就会出现一些复杂的情况。一个电梯状态实质上包含许多子状态(例如，电梯减速、停止、开门、在一段时间后自动关门)。2019/12/15244.2有穷状态机(FSM/FSA)电梯状态M（d，e，f）：电梯e正沿d方向移动，即将到达的是第f层S（d，e，f）：电梯e停在f层，将朝d方向移动（尚未关门）W（e，f）：电梯e在f层等待（已关门）事件DC（e，f）：电梯e在楼层f关上门ST（e，f）：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层电梯是否停下RL（e，f）：f层的电梯按钮或楼层按钮被按下进入打开状态，登录需求2019/12/1525M(d,e,f)：电梯e正沿d方向移动，即将到达的是第f层；S(d,e,f)：电梯e停在f层，将朝d方向移动(尚未关门)W(e,f)：电梯e在f层等待(已关门)其中S(d,e,f)状态已在讨论楼层按钮时定义过，但是，现图4.4是电梯的状态转换图。注意，三个电梯停止状态S(U,e,f)、S(N，e,f)和S(D，e,f)已被组合成一个大的状态，这样做的目的是减少状态总数以简化流图。2019/12/15264.2有穷状态机(FSM/FSA)图4.4电梯的状态转换图2019/12/1527关门之时的规则最后，给出电梯的状态转换规则。为简单起见，这里给出的规则仅发生在关门之时。e停在f层准备向上移动，且门已经关闭，则电梯将向上一楼层移动。第二条和第三条规则，分别对应于电梯即将下降或者没有待处理的请求的情况。S(U,e,f)+DC(e,f)M(U,e,f+1)S(D,e,f)+DC(e,f)M(D,e,f-1)S(N,e,f)+DC(e,f)W(e,f)2019/12/15284.2有穷状态机(FSM/FSA)4.2.3评价有穷状态机描述规格说明：当前状态+事件(+谓词)下个