第3讲-形式化方法及SA的形式化描述

哈尔滨工业大学计算机学院唐好选Email:[e-mail]形式化方法及软件体系结构的形式化描述形式化方法PART1：基本概念形式化方法（FormalMethod）的基本含义是借助数学的方法来研究计算机科学中的有关问题形式化方法提供了一个框架，在框架中可以用数学的方式开发和验证系统。换句话说，在软件开发的全过程中，凡是采用严格的数学语言，具有精确的数学语义的方法，都可称为形式化的方法其中,L：表示形式规格描述语言Cn：表示字符串中的映射,由推理规则组成L,Cn形式化方法的表示形式化方法=形式化系统，语义(1)面向模型的方法：也称为基于状态的形式化方法利用一些已知特性的数学抽象（域、元组、集合、序列、包、映射等）为目标软件的状态特征和行为特征构造模型，如Z(2)代数方法：通过分析不同操作间的行为关系给出操作的隐式定义，而不定义状态，支持描述结构化代数方法仅使用一阶逻辑（包括命题逻辑和谓词逻辑）表示，而不引入通常的数学对象，如:OBJ,CLEAR等语言形式化方法的分类(3)基于进程代数方法：给出并发进程的一个显式模型,并通过进程间的约束来表示行为(4)基于逻辑的方法：采用逻辑描述系统的特性，包括程序行为的低级规范和系统行为规范,如:时态逻辑(5)基于网络的方法：根据网络中的数据流显式地给出系统的并发模型,包括数据在网中从一个结点流向另一个结点的条件.如:Petri网形式化方法的分类上述方法之间的界限并不完全清晰，有些是结合多种方法的多个方面而形成的混成(hybrid)方法大多数方法都以集合论和谓词逻辑作为基础。所以,这些方法在技术上都有相似性。但在表达能力上有一定区别，这也是分类的主要依据形式化方法可通过两种不同方式来使用可用于生成规范，并将此规范作为系统开发基础可将其作为验证系统正确性的依据形式化方法的分类有限状态机Petri网Z方法基于模型的形式化方法通过模型表示系统应满足所定义的行为集合的性质,具体包括：安全性质和活动性质(1)安全性质给出一个性质，对系统的所有执行应保持成立。可用时态逻辑表示安全性：P状态公式，表示性质时态算子，表示“必然”例如：对于命题P：火星上有生命，那么P表示火星上必然有生命基于模型的方法实例R是一非共享资源,N个用户进程使用分配器（AR）管理对资源R的存取用户进程Ui使用资源R前，向AR发出请求，当R可自由存取时，AR作反应标志用户进程Ui使用完R时，向AR发出信号释放R在请求资源到获悉分配到资源间任意时刻，用户进程可取消请求安全需求—系统必须保证在任何时刻R不会分配给多于一个的Ui模型方法的安全性质（例）资源分配器（AR）的规格说明:选择的动作Request(i):Ui请求存取（AR的输入）Cancel(i):Ui取消未完成的请求（AR的输入）Grant(i):Ui被授权获得存取（AR的输出）Finish(i):Ui释放资源（AR的输入）模型方法的安全性质（例）动作类型表示:〈动作名〉WHEN〈条件〉DO〈表达式〉可表示为三元组:(s,a,s’)其中s为状态,由条件决定a为动作名s’由表达式对状态变量赋值决定模型方法的安全性质Ui请求R:Request(i)WHENTrueDoreq[i]:=True取消:Cancel(i)WHENTrueDoreq[i]:=False释放:Finish(i)WHENTrueDogrant[i]:=False被授权:Grant(i)WHEN(req[i]ANDj,Grant[j])Do{Grant(i):=True,req[i]:=False}模型方法的安全性质（例）(2)活动性质断言某事最终必然发生。有了活动，安全性质才有意义。用时态逻辑表示:(PG),即P成立,导致G必然会满足模型满足的活动性质：若任意用户提出请求且未取消，则分配器最终必会授权该用户使用资源有限状态机(FSM,finitestatemachine)一个有限状态机可表示为一个五元组(Q,∑,δ,q0,F)其中:Q:是一个有限、非空状态集;∑:是一个有限、非空输入集;δ:是一个从(Q～F)×∑转换到Q的函数,称为转换函数或变迁函数;q0:q0∈Q是初始状态;F:是最终状态集,FQ每个转换有下列格式当前状态and事件下一个状态扩展FSM可表示为一个六元组(Q,∑,δ,q0,F,P)其中P为一个谓词(Predicate)集,每个谓词是产品的全局状态Y的函数,转换函数δ是从(Q～F)×∑×P转换为Q的函数转换规则:当前状态and事件and谓词下一个状态有限状态机(FSM,finitestatemachine)节点——状态q弧——输入k后状态的变化，由状态qi指向qj的变迁函数表示为：jiqkq),1q3q2q0qaabc开关灯按下关按下开FSM图的一般表示方式有限状态机实例：电梯控制系统m层楼n部电梯的大楼服务系统:每个电梯有一组m个按钮,每层用一个。当按下并让电梯到达相应的层时,这些按钮灯亮，当电梯到达相应层时灯灭除了第一层和顶层,每一层都有两个按钮(请求电梯向上、向下)，按下时灯亮,电梯到达时灯灭没有对电梯请求时,电梯停留在当前楼层,门关闭考虑电梯正常运行情况，电梯处于两个楼层之间时不会停止，并且不会改变运动方向电梯按钮(ElevatorButton,EB)楼层按钮(FloorButton,FB)1)电梯按钮状态图如下：电梯按钮状态EBOFF(e,f)EBON(e,f)EAF(e,f)电梯e到达楼层f电梯按钮关闭电梯按钮开启按下电梯按钮EBP(e,f)定义事件、状态和状态转换规则谓词V(e,f):电梯e到达(停在)楼层f转换规则:(1)当前状态：电梯按钮关，按下按钮(e,f)，电梯e没有到达楼层f。按钮开启EBOFF(e,f)andEBP(e,f)andnotV(e,f)EBON(e,f)(2)若电梯正到达楼层，什么也不发生(3)如果电梯到达楼层f，且按钮处于开启状态,那么关闭电梯按钮EBON(e,f)andV(e,f)EBOFF(e,f)2)楼层按钮(FB)状态图定义谓词S(d,e,f):是一个状态,表示电梯e到达楼层f且移动方向或向上(d=U)、向下(d=D)或挂起(d=N)FBOFF(d,f)FBON(d,f)EAF(1…n,f)电梯1或n到达楼层f楼层按钮的状态按下楼层f按钮,向d方向移动FBP(d,f)使用S(d,e,f),转换规则为:(1)楼层按钮开启条件:楼层f的d方向移动按钮关闭，按下该按钮且无向d方向移动的电梯到达f层FBOFF(d,f)andFBP(d,f)andnotS(d,1…n,f)=FBON(d,f)(2)楼层按钮关闭条件:若该按钮开启,且最少有一个电梯到达楼层f并向d方向移动FBON(d,f)andEAF(1…n,f)andS(d,1…n,f)=FBOFF(d,f),d=U或D谓词V(e,f)，电梯e到达(停在)楼层f也可以定义为:V(ef)=S(U,e,f)orS(D,e,f)3)电梯状态M(d,e,f):电梯e正向d方向移动,即将到达楼层f;S(d,e,f):电梯e停在楼层f;W(e,f):电梯e正在楼层f等待(门关闭);DC(e,f):在楼层f,电梯e的门关闭;ST(e,f):随着电梯e接近楼层f,触发传感器RL:按下按钮S(U,e,f)andDC(e,f)=M(U,e,f+1):电梯e处于状态S(U,e,f)，即停在要上到的楼层,且电梯门关,则该电梯将向上移动到下一层;S(D,e,f)andDC(e,f)=M(D,e,f-1)S(N,e,f)andDC(e,f)=W(e,f)规格说明简单形式:当前状态and事件and谓词=下一个状态电梯的STDM(U,e,f+1)M(D,e,f)S(U,e,f)S(N,e,f)S(D,e,f)M(U,e,f)M(D,e,f-1)W(e,f)ST(e,f)ST(e,f)RLRLDC(e,f)RLRLRLRLRL生产者消费者系统生产者（一个）生产产品/存入仓库消费者（一个）从仓库取出产品/消费产品仓库（两个货位）存库/出库规则如果仓库是满的，生产者进程必须等待，直到消费者进程从仓库中拿走产品，使仓库产生一个空的货位如果仓库是空的，消费者进程必须等待，直到生产者生产一个产品并存入库中生产者消费者系统三个有限状态机描述),},,{},,({M11211PPP存库生产)C,},,{},C,C({M12212消费出库)0,},,{},2,1,0({M33出库入库P1P2生产存库C1C2出库消费0C2入库出库12入库出库生产者消费者系统三个状态机的同步积复合无定义，其余'),(),',,('),(),,',('),(),,,'('),(,'),(),',',('),(,'),(),',,'('),(,'),(),,','('),(,'),(,'),(),',','()a),q,q,q(()Qq,q,q(q0QQQQ)q,,,Q(MMMM3333212223211113213332223213331113212221113213332221113213213020103213210321qaqqqqqaqqqqqaqqqqqaqqaqqqqqaqqaqqqqqaqqaqqqqqaqqaqqaqqqq生产者消费者系统0,P1,C10,P2,C1生产1,P1,C1入库0,P1,C2出库消费0,P2,C2生产1,P2,C1消费生产1,P2,C22,P2,C22,P2,C12,P1,C11,P1,C22,P1,C2入库消费生产消费出库消费生产消费出库入库入库出库有限状态机系统的局限性1.系统的状态数具有状态组合的复杂性问题2.在每一个状态上，任一时刻最多执行一个操作，只能描述顺序系统，不能描述并发系统3.不能描述无限状态系统，缺乏描述时间特性的机制Petri网Petri的特点(1)Petri网是一种数学工具和图形工具(2)Petri网可用于描述系统的不同层次的抽象(3)Petri网可用于描述系统的事件之间因果相关性和不相关性Petri网基本概念简称PNG(PetriNetGraph)是一种有向图,有两种结点:表示状态及状态变化可用三元组N=(P,T,F)表示位置（Place）或称库所集（Places）,符号为,表示系统的状态转移（Transition）或称变迁,符号为“—”或者“|”表示系统中的事件符号“”库所指向变迁，表示事件发生的前提，即对变迁的输入符号“”从变迁指向库所，表示事件的结果，即由变迁的输出标记（token）或称令牌，符号为点燃（fire）符号为使能的(enabled):变迁可以被点燃.库所变迁弧标记输入输出1t2t3t4t5t6t1P2P4P3P5P6P7P1P4P2P3P5P1t2t3t4tPetri网图标记出现，事件t3激发的两个前提已具备，事件t3激发,P3,P5的标记移到P4上定义一：一个Petri网是一个五元组，PN={P,T,A,W,M0},其中：},,,{21nPPPP是一个库所（Place）集P对各弧赋权值},,,{21mtttT是一个变迁（transition）集T)()(PTTPA是一个有向弧集，（P,T,A）构成一个有向图}0{\:NAW},,,{002010nuuuM是一个初始标记（initialmarking）标记用M表示，看成是从库所到自然数N的一个映射NPM:如果niuPMii,,2,1,)(，则说库所中有个令牌（token）iuiP可看成向量，其第个分量表示赋给的令牌个数Mi)(iPMMiPPetri网的基本形式化定义定义二：一个变迁的输入库所集为：}),(|{)(:AtPPtITt简记t*定义三：一个变迁的输出库所集为：}),(|{)(:APtPt