下载

5下载券

加入VIP
  • 专属下载特权
  • 现金文档折扣购买
  • VIP免费专区
  • 千万文档免费下载

上传资料

关闭

关闭

关闭

封号提示

内容

首页 第4章 形式化说明技术

第4章 形式化说明技术 .ppt

第4章 形式化说明技术

懿妧嫕
2011-04-19 0人阅读 举报 0 0 暂无简介

简介:本文档为《第4章 形式化说明技术 ppt》,可适用于IT/计算机领域

概述有穷状态机Petri网Z语言小结作业第章形式化说明技术按照形式化的程度可以把软件工程使用的方法划分成非形式化、半形式化和形式化类。用自然语言描述需求规格说明是典型的非形式化方法。用数据流图或实体联系图建立模型是典型的半形式化方法。所谓形式化方法是描述系统性质的基于数学的技术也就是说如果一种方法有坚实的数学基础那么它就是形式化的。概述非形式化方法的缺点概述非形式化方法的缺点用自然语言书写的系统规格说明书可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。所谓矛盾是指一组相互冲突的陈述。二义性是指读者可以用不同方式理解的陈述。系统规格说明书是很庞大的文档因此几乎不可避免地会出现含糊性。实际上这样笼统的陈述并没有给出任何有用的信息。不完整性可能是在系统规格说明中最常遇到的问题之一。抽象层次混乱是指在非常抽象的陈述中混进了一些关于细节的低层次陈述。这样的规格说明书使得读者很难了解系统的整体功能结构。形式化方法的优点形式化方法的优点为了克服非形式化方法的缺点人们把数学引入软件开发过程创造了基于数学的形式化方法。在开发大型软件系统的过程中应用数学能够带来下述的几个优点:数学最有用的一个性质是它能够简洁准确地描述物理现象、对象或动作的结果因此是理想的建模工具。数学特别适合于表示状态也就是表示“做什么”需求规格说明书主要描述应用系统在运行前和运行后的状态因此数学比自然语言更适于描述详细的需求。在软件开发过程中使用数学可以在不同的软件工程活动之间平滑地过渡。不仅功能规格说明而且系统设计也可以用数学表达程序代码也是一种数学符号。数学作为软件开发工具提供了高层确认的手段。可以使用数学方法证明设计符合规格说明程序代码正确地实现了设计结果。应用形式化方法的准则应用形式化方法的准则人们对形式化方法的看法并不一致。形式化方法对某些软件工程师很有吸引力其拥护者甚至宣称这种方法可以引发软件开发方法的革命另一些人则对把数学引入软件开发过程持怀疑甚至反对的态度。编者认为对形式化方法也应该“一分为二”既不要过分夸大它的优点也不要一概排斥。下面是应用形式化方法的几条准则可在实际工作中使用。()应该选用适当的表示方法。()应该形式化但不要过分形式化。()应该估算成本。()应该有形式化方法顾问随时提供咨询。()不应该放弃传统的开发方法。()应该建立详尽的文档。()不应该放弃质量标准。()不应该盲目依赖形式化方法。()应该测试、测试再测试。()应该重用。有穷状态机概念有穷状态机概念一个简单例子:一个保险箱上装了一个复合锁锁有三个位置分别标记为、、转盘可向左(L)或向右(R)转动。这样在任意时刻转盘都有种可能的运动即L、R、L、R、L和R。保险箱的组合密码是L、R、L转盘的任何其他运动都将引起报警。图描绘了保险箱的状态转换情况。图保险箱的状态转换图图是一个有穷状态机的状态转换图。状态转换并不一定要用图形方式描述表格形式也可以表达同样的信息。从上面这个简单例子可以看出一个有穷状态机包括下述个部分:状态集J、输入集K、由当前状态和当前输入确定下一个状态(次态)的转换函数T、初始态S和终态集F。对于保险箱的例子相应的有穷状态机的各部分如下。状态集J:{保险箱锁定AB保险箱解锁报警}。输入集K:{LRLRLR}。转换函数T:如表所示。初始态S:保险箱锁定。终态集F:{保险箱解锁报警}。如果使用更形式化的术语一个有穷状态机可以表示为一个元组(JKTSF)其中:J是一个有穷的非空状态集K是一个有穷的非空输入集T是一个从(JF)×K到J的转换函数S∈J是一个初始状态FJ是终态集。有穷状态机的概念在计算机系统中应用得非常广泛。例如每个菜单驱动的用户界面都是一个有穷状态机的实现。一个菜单的显示和一个状态相对应键盘输入或用鼠标选择一个图标是使系统进入其他状态的一个事件。状态的每个转换都具有下面的形式:当前状态〔菜单〕事件〔所选择的项〕下个状态。为了对一个系统进行规格说明通常都需要对有穷状态机做一个很有用的扩展即在前述的元组中加入第个组件谓词集P从而把有穷状态机扩展为一个元组其中每个谓词都是系统全局状态Y的函数。转换函数T现在是一个从(JF)×K×P到J的函数。现在的转换规则形式如下:当前状态〔菜单〕事件〔所选择的项〕谓词下个状态。例子例子为了具体说明怎样用有穷状态机技术表达系统的规格说明现在用这种技术给出大家熟悉的电梯系统的规格说明。首先给出用自然语言描述的对电梯系统的需求:在一幢m层的大厦中需要一套控制n部电梯的产品要求这n部电梯按照约束条件CC和C在楼层间移动。C:每部电梯内有m个按钮每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮同时电梯驶向相应的楼层到达按钮指定的楼层时指示灯熄灭。C:除了大厦的最低层和最高层之外每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮当电梯到达此楼层时灯熄灭电梯向要求的方向移动。C:当对电梯没有请求时它关门并停在当前楼层。现在使用一个扩展的有穷状态机对本产品进行规格说明。这个问题中有两个按钮集。n部电梯中的每一部都有m个按钮一个按钮对应一个楼层。因为这m×n个按钮都在电梯中所以称它们为电梯按钮。此外每层楼有两个按钮一个请求向上另一个请求向下这些按钮称为楼层按钮。电梯按钮的状态转换图如图所示。令EB(e,f)表示按下电梯e内的按钮并请求到f层去。EB(e,f)有两个状态分别是按钮发光(打开)和不发光(关闭)。更精确地说状态是:EBON(e,f):电梯按钮(e,f)打开EBOFF(e,f):电梯按钮(e,f)关闭如果电梯按钮(e,f)发光且电梯到达f层该按钮将熄灭。相反如果按钮熄灭则按下它时按钮将发光。上述描述中包含了两个事件它们分别是: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)接下来考虑楼层按钮。令FB(d,f)表示f层请求电梯向d方向运动的按钮楼层按钮FB(d,f)的状态转换图如图所示。楼层按钮的状态如下:FBON(d,f):楼层按钮(d,f)打开FBOFF(d,f):楼层按钮(d,f)关闭如果楼层按钮已经打开而且一部电梯到达f层则按钮关闭。反之如果楼层按钮原来是关闭的被按下后该按钮将打开。这段叙述中包含了以下两个事件。FBP(d,f):楼层按钮(d,f)被按下EAF(…n,f):电梯或…或n到达f层其中…n表示或为或为…或为n。为了定义与这些事件和状态相联系的状态转换规则同样也需要一个谓词它是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,…n,f)FBON(d,f)FBON(d,f)EAF(…n,f)S(d,…n,f)FBOFF(d,f)其中d=UorD。也就是说如果在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)定义电梯按钮和楼层按钮的状态都是很简单、直观的事情。现在转向讨论电梯的状态及其转换规则就会出现一些复杂的情况。一个电梯状态实质上包含许多子状态。下面定义电梯的个状态:M(d,e,f):电梯e正沿d方向移动即将到达的是第f层S(d,e,f):电梯e停在f层将朝d方向移动(尚未关门)W(e,f):电梯e在f层等待(已关门)其中S(d,e,f)状态已在讨论楼层按钮时定义过但是现在的定义更完备一些。图是电梯的状态转换图。个电梯停止状态S(U,e,f)、S(N,e,f)和S(D,e,f)已被组合成一个大的状态这样做的目的是减少状态总数以简化流图。图中包含了下述个可触发状态发生改变的事件。DC(e,f):电梯e在楼层f关上门ST(e,f):电梯e靠近f层时触发传感器电梯控制器决定在当前楼层电梯是否停下RL:电梯按钮或楼层按钮被按下进入打开状态登录需求图电梯的状态转换图最后给出电梯的状态转换规则。为简单起见这里给出的规则仅发生在关门之时。S(U,e,f)DC(e,f)M(U,e,f)S(D,e,f)DC(e,f)M(D,e,f)S(N,e,f)DC(e,f)W(e,f)第一条规则表明如果电梯e停在f层准备向上移动且门已经关闭则电梯将向上一楼层移动。第二条和第三条规则分别对应于电梯即将下降或者没有待处理的请求的情况。评价评价有穷状态机方法采用了一种简单的格式来描述规格说明:当前状态事件谓词下个状态这种形式的规格说明易于书写、易于验证而且可以比较容易地把它转变成设计或程序代码。事实上可以开发一个CASE工具把一个有穷状态机规格说明直接转变为源代码。维护可以通过重新转变来实现也就是说如果需要一个新的状态或事件首先修改规格说明然后直接由新的规格说明生成新版本的产品。有穷状态机方法比数据流图技术更精确而且和它一样易于理解。不过它也有缺点:在开发一个大系统时三元组(即状态、事件、谓词)的数量会迅速增长。此外和数据流图方法一样形式化的有穷状态机方法也没有处理定时需求。下节将介绍的Petri网技术是一种可处理定时问题的形式化方法。Petri网概念Petri网概念并发系统中遇到的一个主要问题是定时问题。这个问题可以表现为多种形式如同步问题、竞争条件以及死锁问题。定时问题通常是由不好的设计或有错误的实现引起的而这样的设计或实现通常又是由不好的规格说明造成的。如果规格说明不恰当则有导致不完善的设计或实现的危险。用于确定系统中隐含的定时问题的一种有效技术是Petri网这种技术的一个很大的优点是它也可以用于设计中。Petri网是由CarlAdamPetri发明的。最初只有自动化专家对Petri网感兴趣后来Petri网在计算机科学中也得到广泛的应用例如在性能评价、操作系统和软件工程等领域Petri网应用得都比较广泛。特别是已经证明用Petri网可以有效地描述并发活动。Petri网包含种元素:一组位置P、一组转换T、输入函数I以及输出函数O。图举例说明了Petri网的组成。图Petri网的组成一组位置P为{PPPP}在图中用圆圈代表位置。一组转换T为{tt}在图中用短直线表示转换。两个用于转换的输入函数用由位置指向转换的箭头表示它们是:I(t)={PP}I(t)={P}两个用于转换的输出函数用由转换指向位置的箭头表示它们是:O(t)={P}O(t)={PP}注意输出函数O(t)中有两个P是因为有两个箭头由t指向P。更形式化的Petri网结构是一个四元组C=(P,T,I,O)。其中P={P…Pn}是一个有穷位置集n≥。T={t…tm}是一个有穷转换集m≥且T和P不相交。I:T→P∞为输入函数是由转换到位置无序单位组(bags)的映射。O:T→P∞为输出函数是由转换到位置无序单位组的映射。一个无序单位组或多重组是允许一个元素有多个实例的广义集。Petri网的标记是在Petri网中权标(token)的分配。例如在图中有个权标其中一个在P中两个在P中P中没有还有一个在P中。上述标记可以用向量()表示。由于P和P中有权标因此t启动(即被激发)。通常当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时就允许转换。当t被激发时P和P上各有一个权标被移出而P上则增加一个权标。Petri网中权标总数不是固定的在这个例子中两个权标被移出而P上只能增加一个权标。在图中P上有权标因此t也可以被激发。当t被激发时P上将移走一个权标而P上新增加两个权标。Petri网具有非确定性也就是说如果数个转换都达到了激发条件则其中任意一个都可以被激发。图所示Petri网的标记为()t和t都可以被激发。假设t被激发了则结果如图所示标记为()。此时只有t可以被激发。如果t也被激发了则权标从P中移出两个新权标被放在P上结果如图所示标记为()。图带标记的Petri网图图的Petri网在转换t被激发后的情况图图的Petri网在转换t被激发后的情况图含禁止线的Petri网更形式化地说Petri网C=(PTIO)中的标记M是由一组位置P到一组非负整数的映射:M:P→{…}这样带有标记的Petri网成为一个五元组(PTIOM)。对Petri网的一个重要扩充是加入禁止线。如图所示禁止线是用一个小圆圈而不是用箭头标记的输入线。通常当每个输入线上至少有一个权标而禁止线上没有权标的时候相应的转换才是允许的。在图中P上有一个权标而P上没有权标因此转换t可以被激发。例子例子现在把Petri网应用于上一节讨论过的电梯问题。当用Petri网表示电梯系统的规格说明时每个楼层用一个位置Ff代表(≤f≤m)在Petri网中电梯是用一个权标代表的。在位置Ff上有权标表示在楼层f上有电梯。电梯按钮电梯问题的第一个约束条件描述了电梯按钮的行为现在复述一下这个约束条件。第一条约束C:每部电梯有m个按钮每层对应一个按钮。当按下一个按钮时该按钮指示灯亮指示电梯移往相应的楼层。当电梯到达指定的楼层时按钮将熄灭。为了用Petri网表达电梯按钮的规格说明在Petri网中还必须设置其他的位置。电梯中楼层f的按钮在Petri网中用位置EBf表示(≤f≤m)。在EBf上有一个权标就表示电梯内楼层f的按钮被按下了。电梯按钮只有在第一次被按下时才会由暗变亮以后再按它则只会被忽略。图所示的Petri网准确地描述了电梯按钮的行为规律。首先假设按钮没有发亮显然在位置EBf上没有权标从而在存在禁止线的情况下转换“EBf被按下”是允许发生的。假设现在按下按钮则转换被激发并在EBf上放置了一个权标如图所示。以后不论再按下多少次按钮禁止线与现有权标的组合都决定了转换“EBf被按下”不能再被激发了因此位置EBf上的权标数不会多于。图Petri网表示的电梯按钮假设电梯由g层驶向f层因为电梯在g层如图所示位置Fg上有一个权标。由于每条输入线上各有一个权标转换“电梯在运行”被激发从而EBf和Fg上的权标被移走按钮EBf被关闭在位置Ff上出现一个新权标即转换的激发使电梯由g层驶到f层。事实上电梯由g层移到f层是需要时间的为处理这个情况及其他类似的问题(例如由于物理上的原因按钮被按下后不能马上发亮)Petri网模型中必须加入时限。也就是说在标准Petri网中转换是瞬时完成的而在现实情况下就需要时间控制Petri网以使转换与非零时间相联系。楼层按钮在第二个约束条件中描述了楼层按钮的行为。第二条约束C:除了第一层与顶层之外每个楼层都有两个按钮一个要求电梯上行另一个要求电梯下行。这些按钮在按下时发亮当电梯到达该层并将向指定方向移动时相应的按钮才会熄灭。在Petri网中楼层按钮用位置FBfu和FBfd表示分别代表f楼层请求电梯上行和下行的按钮。底层的按钮为FBu最高层的按钮为FBmd中间每一层有两个按钮FBfu和FBfd(<f<m)。图Petri网表示楼层按钮图所示的情况为电梯由g层驶向f层。根据电梯乘客的要求某一个楼层按钮亮或两个楼层按钮都亮。如果两个按钮都亮了则只有一个按钮熄灭。图所示的Petri网可以保证当两个按钮都亮了的时候只有一个按钮熄灭。但是要保证按钮熄灭正确则需要更复杂的Petri网模型。最后考虑第三条约束。第三条约束C:当电梯没有收到请求时它将停留在当前楼层并关门。这条约束很容易实现如图所示当没有请求(FBfu和FBfd上无权标)时任何一个转换“电梯在运行”都不能被激发。Z语言简介Z语言简介用Z语言描述的、最简单的形式化规格说明含有下述个部分:给定的集合、数据类型及常数。状态定义。初始状态。操作。给定的集合一个Z规格说明从一系列给定的初始化集合开始。所谓初始化集合就是不需要详细定义的集合这种集合用带方括号的形式表示。对于电梯问题给定的初始化集合称为Button即所有按钮的集合因此Z规格说明开始于:〔Button〕状态定义一个Z规格说明由若干个“格(schema)”组成每个格含有一组变量说明和一系列限定变量取值范围的谓词。例如格S的格式如图所示。图Z格S的格式在电梯问题中Button有个子集即floorbuttons(楼层按钮的集合)、elevatorbuttons(电梯按钮的集合)、buttons(电梯问题中所有按钮的集合)以及pushed(所有被按的按钮的集合即所有处于打开状态的按钮的集合)。图(见书页)描述了格ButtonState其中符号P表示幂集(即给定集的所有子集)。约束条件声明floorbuttons集与elevatorbuttons集不相交而且它们共同组成buttons集(在下面的讨论中并不需要floorbuttons集和elevatorbuttons集把它们放于图中只是用来说明Z格包含的内容)。初始状态抽象的初始状态是指系统第一次开启时的状态。对于电梯问题来说抽象的初始状态为:ButtonInit〔ButtonState|pushed=Φ〕上式表示当系统首次开启时pushed集为空即所有按钮都处于关闭状态。操作如果一个原来处于关闭状态的按钮被按下则该按钮开启这个按钮就被添加到pushed集中。图(见书页)定义了操作PushButton(按按钮)。操作的谓词部分包含了一组调用操作的前置条件以及操作完全结束后的后置条件。如果前置条件成立则操作执行完成后可得到后置条件。但是如果在前置条件不成立的情况下调用该操作则不能得到指定的结果(因此结果无法预测)。假设电梯到达了某楼层如果相应的楼层按钮已经打开则此时它会关闭同样如果相应的电梯按钮已经打开则此时它也会关闭。也就是说如果“button”属于pushed集则将它移出该集合如图(见书页)所示(符号“\”表示集合差运算)。评价评价已经在许多软件开发项目中成功地运用了Z语言目前Z也许是应用得最广泛的形式化语言尤其是在大型项目中Z语言的优势更加明显。Z语言之所以会获得如此多的成功主要有以下几个原因:()可以比较容易地发现用Z写的规格说明的错误特别是在自己审查规格说明及根据形式化的规格说明来审查设计与代码时情况更是如此。()用Z写规格说明时要求作者十分精确地使用Z说明符。由于对精确性的要求很高从而和非形式化规格说明相比减少了模糊性、不一致性和遗漏。()Z是一种形式化语言在需要时开发者可以严格地验证规格说明的正确性。()虽然完全学会Z语言相当困难但是经验表明只学过中学数学的软件开发人员仍然可以只用比较短的时间就学会编写Z规格说明当然这些人还没有能力证明规格说明的结果是否正确。()使用Z语言可以降低软件开发费用。虽然用Z写规格说明所需用的时间比使用非形式化技术要多但开发过程所需要的总时间却减少了。()虽然用户无法理解用Z写的规格说明但是可以依据Z规格说明用自然语言重写规格说明。经验证明这样得到的自然语言规格说明比直接用自然语言写出的非形式化规格说明更清楚、更正确。使用形式化规格说明是全球的总趋势过去主要是欧洲习惯于使用形式化规格说明技术现在越来越多的美国公司也开始使用形式化规格说明技术。小结小结基于数学的形式化规格说明技术目前还没有在软件产业界广泛应用但是与欠形式化的方法比较起来它确实有实质性的优点:形式化的规格说明可以用数学方法研究、验证此外形式化的规格说明消除了二义性而且它鼓励软件开发者在软件工程过程的早期阶段使用更严格的方法从而可以减少差错。形式化方法的缺点:大多数形式化的规格说明主要关注于系统的功能和数据而问题的时序、控制和行为等方面的需求却更难于表示。此外形式化方法比欠形式化方法更难学习不仅在培训阶段要花大量的投资而且对某些软件工程师来说它代表了一种“文化冲击”。把形式化方法和欠形式化方法有机地结合起来使它们取长补短应该能获得更理想的效果。作业作业P

用户评价(0)

关闭

新课改视野下建构高中语文教学实验成果报告(32KB)

抱歉,积分不足下载失败,请稍后再试!

提示

试读已结束,如需要继续阅读或者下载,敬请购买!

文档小程序码

使用微信“扫一扫”扫码寻找文档

1

打开微信

2

扫描小程序码

3

发布寻找信息

4

等待寻找结果

我知道了
评分:

/60

第4章 形式化说明技术

VIP

在线
客服

免费
邮箱

爱问共享资料服务号

扫描关注领取更多福利