第7讲形式化说明技术ppt课件

1、第4章形式化说明技术什么是形式化说明技术l从广义上讲，形式化方法是指将离散数学的方法用于解决软件工程领域的问题，主要包括建立精确的数学模型以及对模型的分析活动。l狭义的讲，形式化方法是运用形式化语言，进行形式化的规格描述、模型推理和验证的方法。l就形式化建模而言，形式化表示必须包含一组定义其语法语义的形式化规则。这些规则可用于分析给定的表达式是否符合语法规定，或证明该表达式具有某种性质。形式化说明技术l用自然语言描述需求规格说明，是典型的非形式化方法。用数据流图或ER图建立模型，是典型的半形式化方法。所谓形式化方法，就是基于数学的技术来描述系统的性质的方法。l非形式化方法的缺点l形式化方法的优

2、点应用形式化方法的准则(1) 应该选用适当的表示方法。(2) 应该形式化，但不要过分形式化。(3) 应该估算成本。(4) 应该有形式化方法顾问随时提供咨询。 (5) 不应该放弃传统的开发方法。把形式化方法和结构化方法或面向对象方法集成起来是可能的，而且由于 取长补短往往能获得很好的效果。 (6) 应该建立详尽的文档。建议使用自然语言注释形式化的规格说明书，以帮助用户和维护人员理解系统。 (9) 应该测试、测试再测试。 (10) 应该重用。即使采用了形式化方法，软件重用仍然是降低软件成本和提高软件质量的惟一合理的方法。而且用形式化方法说明的软件构件具有清晰定义的功能和接口，使得它们有更好的可重用

3、性。 有穷状态机l例子：保险箱的复合锁，锁有三个位置，分别标记为1，2，3，转盘可向左L或向右R转动。l任意时刻的6种可能的运动：1R,1L,2R,2L,3R,3Ll假设组合密码为：1L,3R,2L，除了这个次序的任意转动都将导致报警。保险箱锁定AB保险箱解锁报警1L转盘的任何其他移动3R2L转盘的任何其他移动转盘的任何其他移动初始态终态终态 当前状态 次态 转盘动作 保险箱锁定AB1LA报警报警1R报警报警报警2L报警报警保险箱解锁2R报警报警报警3L报警报警报警3R报警B报警状态集状态集J：保险箱锁定，保险箱锁定，A，B，保险箱解锁，报警，保险箱解锁，报警。输入集：输入集：1L，1R，2L

4、，2R，3L，3R转换函数：转换函数：T初始态初始态S：保险箱锁定。：保险箱锁定。终态集：终态集：保险箱解锁，报警保险箱解锁，报警l一个有穷状态机可以表示为一个5元组J，K，T，S，FlJ是一个有穷的非空状态集lK是一个有穷的非空输入集lT是一个从J-F）*K到J的转换函数lSJ，是一个初始状态lF J，是终态集l例如：菜单l一个菜单的显示和一个状态相对应l键盘输入或鼠标点击对应于一个事件l当前状态菜单+事件所选择的项+谓词=下个状态电梯的例子l电梯的约束条件：lC1：每部电梯有m个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯灭

5、。lC2：除了楼的最低层和最高层外，每层楼有两个按钮分别指示是上楼还是下楼。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。lC3：当对电梯没有请求时，它关门并停在当前楼层。电梯按钮lEBe,f） ：表示按下电梯e内的按钮并请求到f层去lEBPe,f）:电梯按钮(e,f)被按下lEAFe,f）:电梯e到达f层l谓词：V(e,f):电梯停在f层l如果电梯按钮(e,f)处于关闭状态当前状态，而且电梯(e,f)被按下事件，而且电梯e不在f层谓词，则该电梯按钮打开发光下个状态。状态转换规则的形式化描述如下：lEBOFF(e,f)+EBP(e,f)+not V(e,

6、f)=EBON(e,f)lEBON(e,f)+EAF(e,f)=EBOFF(e,f)EBOFF(e,f)EBON(e,f)EBP(e,f)EAF(e,f)楼层按钮lFB(d,f)表示f层请求电梯向d方向运动的按钮lFBON(d,f):楼层按钮(d,f)翻开 FBOFF(d,f)：楼层按钮(d,f)关闭lFBP(d,f):楼层按钮(d,f)被按下 EAF(1n,f):电梯1或或n到达f层lS(d,e,f)：电梯e停在f层并且移动方向由d确定为向上(d=U)或向下(d=D)或待定(d=N)l状态转换规则：lFBOFF(d,f)+FBP(d,f)+not S(d,1n,f)=FBON(d,f)lFB

7、ON(d,f)+EAF(1n,f)+S(d,1n,f)=FBOFF(d,f)FBOFF(d,f)FBON(d,f)FBP(d,f)EAF(1n,f)lV(e,f)=S(U,e,f) or S(D,e,f) or S(N,e,f)l电梯的三个状态：lM(d,e,f)：电梯e正沿d方向移动，即将到达的是第f层lS(d,e,f)：电梯e停在f层，将朝d方向移动(尚未关门)lW(e,f):电梯e在f层等待(已关门)l可触发状态发生改变的事件lDC(e,f):电梯e在楼层f关上门lST(e,f):电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层电梯是否停下lRL：电梯按钮或楼层按钮被按下进入打开状态

8、，登录需求l电梯的状态转换规则lS(U,e,f)+DC(e,f)=M(U,e,f+1)lS(D,e,f)+DC(e,f)=M(D,e,f-1)lS(N,e,f)+DC(e,f)=W(e,f)S(U,e,f)S(N,e,f)M(U,e,f+1)S(D,e,f)M(D,e,f)M(U,e,f)M(D,e,f-1)W(e,f)DC(e,f)RLRLST(e,f)RLRLRLDC(e,f)DC(e,f)ST(e,f)Petri网lPetri网是用于形式化说明定时问题的一种技术l一组位置 P 为 P1 ， P2 ， P3 ， P4 ，在图中用圆圈代表位置。 l一组转换 T 为 t1 ， t2 ，在图中用

9、短直线表示转换。 l两个用于转换的输入函数，用由位置指向转换的箭头表示，它们是： lI(t1)= P2 ， P4 I(t2)= P2 l两个用于转换的输出函数，用由转换指向位置的箭头表示，它们是: lO(t1)= P1 O(t2)= P3 ， P3 p1p2p4t2t1p3lPetri网包含4种元素：一组位置P、一组转换T、输入函数I以及输出函数O。lPetri网结构，是一个四元组C=(P,T,I,O)lP=P1,Pn是一个有穷位置集lT=t1,tm是一个有穷转换集l I：T-P 为输入函数，是由转换到位置组的映射lO： T-P 为输出函数，是由转换到位置组的映射p1p2p4t2t1p3p1p

10、2p4t2t1p3标志：(1,2,0,1)标志：(2,1,0,0)标志：(2,0,2,0)p1p2p4t2t1p3权标权标lPetri网的标记M，是由一组位置P到一组非负整数的映射：lM：P-0,1,2l所以，Petri网成为一个五元组P,T,I,O,M）p1p2p3t1对Petri网的扩充：加入禁止线。禁止线是用一个圆圈而不是用箭头标记的输入线。通常。当每个输入线上至少有一个权标，而禁止线上没有权标的时候，相应的转换才是允许的。lC1:每部电梯有m个按钮，每层对应一个按钮。当按下一个按钮时该按钮指示灯亮，指示电梯移往相应的楼层。当电梯到达指定的楼层时，按钮熄灭。l电梯中楼层f的按钮，在Pet

11、ri网中用位置EBf表示。(1fm)。在EBf上有一个权标，表示电梯内楼层f的按钮被按下了。FgFfEBfEBf被按下电梯在运行电梯在运行电梯按钮只有在第一次被按下时才会由暗变亮，以后电梯按钮只有在第一次被按下时才会由暗变亮，以后再按它会被忽略。再按它会被忽略。 假设按钮没有亮，在位置假设按钮没有亮，在位置Ebf上没有权标，那么上没有权标，那么在存在禁止线的情况下，转换在存在禁止线的情况下，转换“EBf是允许发生的。是允许发生的。按下按钮之后，则转换被激发并在按下按钮之后，则转换被激发并在EBf上放置了一个权上放置了一个权标，以后无论再按下多少次按钮，禁止线与现有权标标，以后无论再按下多少次按

12、钮，禁止线与现有权标的组合都决定了转换的组合都决定了转换“EBf被按下不能再被激发了，被按下不能再被激发了，因而，位置因而，位置EBf上的权标数不会多于上的权标数不会多于1图4.11 Petri网表示楼层按钮4 Z语言简介语言简介用用Z Z语言描述的、最简单的形式化规格说明含有下述语言描述的、最简单的形式化规格说明含有下述4 4个部个部分：分：给定的集合、数据类型及常数。给定的集合、数据类型及常数。状态定义。状态定义。初始状态。初始状态。操作。操作。l1. 1. 给定的集合给定的集合l一个一个Z Z规格说明从一系列给定的初始化集合开始。所谓初始化集合就规格说明从一系列给定的初始化集合开始。所谓

13、初始化集合就是不需要详细定义的集合，这种集合用带方括号的形式表示。对于电是不需要详细定义的集合，这种集合用带方括号的形式表示。对于电梯问题，给定的初始化集合称为梯问题，给定的初始化集合称为ButtonButton，即所有按钮的集合，因而，即所有按钮的集合，因而，Z Z规格说明开始于：规格说明开始于：ButtonButtonl2. 2. 状态定义状态定义l一个一个Z Z规格说明由若干个规格说明由若干个“格格(schema)”(schema)”组成，每个格含有一组变量组成，每个格含有一组变量说明和一系列限定变量取值范围的谓词。例如，说明和一系列限定变量取值范围的谓词。例如，Z Z格格S S的格式如

14、图的格式如图4.124.12所示。所示。在电梯问题中，在电梯问题中，ButtonButton有有4 4个子集，个子集，floor_buttons(floor_buttons(楼层按钮的集合楼层按钮的集合) )elevator_buttons(elevator_buttons(电梯按钮的集合电梯按钮的集合) )buttons(buttons(电梯问题中所有按钮的集合电梯问题中所有按钮的集合) )pushed(pushed(所有被按的按钮的集合，即所有处于打开状态的按钮的集合所有被按的按钮的集合，即所有处于打开状态的按钮的集合) )。3. 初始状态抽象的初始状态是指系统第一次开启时的状态。对于电梯

15、问题来说，抽象的初始状态为：Button_Init Button_Statepushed=上式表示，当系统首次开启时pushed集为空，即所有按钮都处于关闭状态。4. 操作如果一个原来处于关闭状态的按钮被按下，则该按钮开启，这个按钮就被添加到pushed集中。 Button_Statebutton?: button(button? buttons)(button? pushed) (pushed= pushedbutton?) (button? pushed) (pushed= pushed)Button_Statebutton?: button(button? buttons)(button

16、? pushed) (pushed= pushedbutton?) (button? pushed) (pushed= pushed)Push_buttonFloor_ArrivalZ 语言实例：停车场管理系统语言实例：停车场管理系统l基本数据类型定义l“停车提示是一个基本数据类型的名字l“停好和“停车场满是该类型的数据可能的取值l停车提示= 停好| 停车场满l全局变量声明l在Z 语言中，N 和Z 属于基本数据集合，分别表示正整数集合和整数集合。l停车场容量: Z/*变量声明*/l停车场容量0/*变量约束*/l状态定义l每个系统有唯一的状态定义，可以为状态命名。本例中为系统状态命名为“停车场状

17、态”。状态定义中首先声明一或多个表示系统状态的变量，这里的变量名为“停车数量”，类型为整数。该变量的约束条件为取值大于等于0，小于等于最大停车数量。l停车场状态l停车数量: Z/*状态变量声明*/l停车数量0l停车数量停车场容量l初始化l定义系统状态变量的初始值。系统的初始化定义是唯一的。l操作定义l每个系统可以定义若干个操作。lZ 语言中操作的定义是基于状态的，而不是基于过程的。l该操作如何改变了系统的状态变量的值？l该操作有哪些输入变量？l有哪些输出变量？l当一个操作改变了某个系统状态变量x时，在操作定义的第一行写出状态变化声明x。l当一个操作未改变任何系统状态变量时，即可以在操作定义第一

18、行写出以下状态声明状态变量可省略）。l操作定义续）l操作定义也可以采用以下形式l进入停车场 正常停车停车场满l表示：l操作“进入停车场分为“正常停车和“停车场满两种可能情况，具体执行时选择哪种情况，由环境满足哪种操作的约束条件来决定。评价Z Z语言优势：语言优势：(1) (1) 可以比较容易地发现用可以比较容易地发现用Z Z写的规格说明的错误，特别是在自己审写的规格说明的错误，特别是在自己审查规格说明，及根据形式化的规格说明来审查设计与代码时，情况更查规格说明，及根据形式化的规格说明来审查设计与代码时，情况更是如此。是如此。(2) (2) 用用Z Z写规格说明时，要求作者十分精确地使用写规格说明时，要求作者十分精确地使用Z Z说明符。由于对精说明符。由于对精确性的要求很高，从而和非形式化规格说明相比，减少了模糊性、不确性的要求很高，从而和非形式化规格说明相比，减少了模糊性、不一致性和遗漏。一致性和遗漏。 (3) Z(3) Z是一种形式化语言，在需要时开发者可以严格地验证规格说明是一种形式化语言，在需要时开发者可以严格地验证规格说明的正确性。的正确性。(4) (4