第2章有限状态机及其扩展ppt课件.ppt

1,Chapter 2 有限状态机及其扩展,有限状态机 有限状态机是有限计算的基本模型，也是许多形式化规格、验证方法的基础模型。 Statecharts Statecharts是通过定义递阶状态、状态的AND或OR分解等高级特性的有限状态机的一种扩展形式。,2,（一） 有限状态机,（1） 基本概念 有限状态机（finite state machine）或有限自动机（finite automata）是有限计算的基本模型，是许多形式化规格、验证方法的基础模型。,超级商场的自动门控制器 自动门的前、后分别有两个缓冲区。自动门的前缓冲区用来检测是否有人接近。自动门的后缓冲区，使得控制器把门打开足够长的时间让人走进去，并且不让门在打开的时候碰到站在它附近的人。自动门控制器依据前缓冲区、后缓冲区的检测信息给出打开或闭合的动作指令。 自动门的动作控制应满足如下要求（规格）： 当前缓冲区和后缓冲区均无顾客出现，则自动门处于闭合状态； 当后缓冲区有顾客出现，则自动门维持其原有状态； 当前缓冲区有顾客且后缓冲区无顾客，则打开自动门。,（1） 基本概念,状态集合Q = closed, open；初始状态 q0 = closed；输入集合 = front, rear, both, neither状态转移关系集合 (closed, rear) =closed；(closed,both)=closed；(closed, neither)=closed；(closed,front)=open(open, rear) = pen； (open,both) =open； (open, front) = open；(open, neither) = closedclosed：闭合状态； open：打开状态；front：前缓冲区有顾客；rear：后缓冲区有顾客；both = front rear：前、后缓冲区都有顾客；neither = front rear：前、后缓冲区都无顾客,4,（1） 基本概念,模3计数器 状态集合Q = 0, 1, 2 ；初始状态 q0 = 0；输入集合 = inc, dec状态转移关系集合(0,inc)=1；(0,dec)=2；(1,inc)=2；(1,dec)=0；(2,inc)=0；(2,dec)=1,inc：增加1dec：减少1,5,（1） 基本概念,身份认证系统 （合法身份：ABA） 状态集合Q = 1, 2, 3, 4 ； 初始状态 q0 = 1； 终结状态集合 F = 4； 输入集合 = A, B, C 状态转移关系集合 (1,A)=2；(1,B)=1；(1,C) =1；(2,A)=2；(2,B)=3；(2,C) =1；(3,A) =4；(3,B)=1；(3,C) =1 ABCACA AABCABA ,6,（1） 基本概念,有限状态机是一个五元组 M = (Q, , , q0, F)，其中 Q = q0, q1, qn是有限状态集合。在任一确定的时刻，有限状态机只能处于一个确定的状态qi； = 1,2, m是有限输入字符集合。在任一确定的时刻，有限状态机只能接收一个确定的输入j； ：Q Q是状态转移函数。如果在某一确定的时刻，有限状态机处于某一状态qiQ，并接收一个输入字符j，那么下一时刻将处于一个确定的状态q = (qi，j)Q。在这里规定q = (q，) ； q0 Q是初始状态，有限状态机由此状态开始接收输入； F Q是终结状态集合，有限状态机在达到终结态后不再接收输入。,7,（1） 基本概念,一个有限状态机包括：一个有限状态集，用于描述系统中的不同状态；一个输入符号集，用于表征系统所接收的不同输入信息；一个状态转移函数，用于表述系统在接收不同输入下,从一个状态转移到另外一个状态的规则。 状态转移函数:刻画其行为的最关键部分, 一个从Q到Q的二元函数。状态转移函数通常可以用关系矩阵、状态转移表或状态转移图的形式来表示。有限状态机可用四元组 M = (Q, , , q0)或三元组 M = (Q, , )来表示。,8,（1） 基本概念,状态转移矩阵 用行表示状态机所处的当前状态，列表示将要到达的下一个状态，行列交叉处表示输入字符。称该矩阵为转移函数的关系矩阵，或者有限状态机M 的状态转移矩阵。,模3计数器,9,状态转移表 用表格的行表示状态机所处的当前状态，列表示当前的输入字符，行列交叉处表示要到达的下一个状态。称该表格为M的状态转换表。,模3计数器,10,状态转移图 用圆圈（结点）表示状态；将存在转移关系的状态用有向弧连接，并标注相应的输入字符在有向弧旁；用标有箭头的结点表示初始状态；属于终结状态集中的状态用双圈表示。,模3计数器,11,（1） 基本概念,前面讨论的有限状态机，可以看作仅接受输入符号并发生状态改变，但无任何输出的自动机器。现实生活中的许多有限状态系统,对于不同的输入信号，除内部状态不断改变外，还不断向系统外部输出各种信号。将有限状态机进行推广，引出具有输出机制的自动机器模型。带输出的自动机器模型，按照输出的不同分成两类：输出与状态有关Moore机；输出与状态和输入有关Mealy机。,12,（1） 基本概念,Moore机形式定义为六元组M = (Q, , , , , q0)，其中 Q = q0,q1,qn是有限状态集合； = 1,2,m是有限输入字符集合； = a1,a2,ar是有限输出字符集合； ：Q Q是状态转移函数； ：Q 是输出函数； q0 Q是初始状态。,例：模3余数Q = q0，q1，q2= 0，1(qj) = j, j = 0,1,2,在输入010100 下，输出为012212,13,（1） 基本概念,Mealy机形式定义为六元组M = (Q, , , , , q0)，其中 Q = q0,q1,qn是有限状态集合； = 1,2,m是有限输入字符集合； = a1,a2,ar是有限输出字符集合； ：Q Q是状态转移函数； ：Q 是输出函数； q0 Q 是初始状态。,状态转移函数为：(q0,0) = q1, (q0,1) = q2, (q1,1) = q2, (q1,0) = q1, (q2,1) = q2, (q2,0) = q1输出函数为： (q0,0) = n, (q0,1) = n, (q1,1) = n, (q1,0) = y, (q2,1) = y, (q2,0) = n。在输入01100 下，输出为nnyny,14,（1） 基本概念,身份认证系统（具有条件和变量机制的有限状态机）(最大允许错误次数为3)（err：报警状态； ctr：计数变量）Xcon/Yexec含义在于：所标注的状态转移关系在输入x且条件con成立下，转移至下一状态，并输出y且执行exec。标注中的各项x、con、y或exec可以缺省。,1,2,A,3,B,Cctr3/ctr:=ctr+1,B,A,4,err,Cctr3/ctr:=ctr+1,B,Cctr=3/ctr:=ctr+1,B,Cctr=3/ctr:=ctr+1,A,Cctr=3/ctr:=ctr+1,B,Cctr3/ctr:=ctr+1,Actr3/ctr:=ctr+1,/ctr:= 0,15,（1） 基本概念,身份认证系统,16,（2） 有限状态机的复合,通常，软件系统是以模块或子系统的形式出现整个软件系统的有限状态机规格,需要对各个模块的有限状态机进行复合。有限状态机复合的最简单方式是笛卡尔积有限状态机的笛卡尔积复合,规格了多个有限状态机相互独立运行的行为。软件系统之间存在交互问题，有限状态机的复合也必然涉及交互问题。,17,（2） 有限状态机的复合,有限状态机M1 = (Q1, 1, 1, q10)和M2 = (Q2, 2, 2, q20) 的笛卡尔积为M = M1 M2 = (Q, , , q0)，其中， Q = Q1Q2； = (1 )(2 )； q0 = (q10, q20) Q1Q2； (q1, q2), (a1, a2) = (q1, q2) 1(q1, a1)=q1，a2 = ，a11 (q1, q2) 2(q2, a2)=q2，a1 = ，a22 (q1, q2) 1(q1, a1)=q1，2(q2, a2)=q2，a11，a22 无定义 其余,18,（2） 有限状态机的复合,模3计数器,模4计数器,模3和模4计数器的笛卡尔积复合有34=12个状态每个状态下，两个模计数器均可相互独立地进行加数、减数或保持不变,19,（2） 有限状态机的复合,每个状态有33=9种状态转移选择，但其中一种为无任何状态转移发生，故只有8种状态转移。其笛卡尔积复合具有128=96个状态转移,模计数器的笛卡尔积复合,20,有限状态机的同步积复合,有限状态机M1 = (Q1, 1, 1, q10)和M2 = (Q2, 2, 2, q20) 的同步积复合为M = M1 M2 = (Q, , , q0)，其中， Q = Q1Q2； = 1 2 ； q0 = (q10, q20) Q1Q2； (q1, q2), a) = (q1, q2) 1(q1, a)=q1， 2(q2, a)=q2，a1 2 (q1, q2) 2(q2, a)=q2，a1，a2 (q1, q2) 1(q1, a)=q1，a1，a2 无定义 其余,21,有限状态机的同步积复合,模计数器的同步积复合,模3和模4计数器，可以进行耦合运行，阻止各自的独立运行行为。只有inc、inc和dec、dec两种共24个状态转移,22,有限状态机的异步积复合,有限状态机M1 = (Q1, 1, 1, q10)和M2 = (Q2, 2, 2, q20) 的异步积复合为M = M1 M2 = (Q, , , q0)，其中， Q = Q1Q2； = 1 2 ； q0 = (q10, q20) Q1Q2； (q1, q2), a) = (q1, q2) 2(q2, a)=q2，a2 (q1, q2) 1(q1, a)=q1，a1 无定义 其余,23,有限状态机的异步积复合,模计数器的异步积复合,模3和模4计数器，可以进行耦合运行，但在任何状态下仅有其中一个模计数器运行。 分别有inc和dec两种共48个状态转移,（3） 生产者-消费者问题,生产者消费者系统包含一个生产者和一个消费者。生产者进程产生消息，并把产生的消息写入一个能容纳两个消息的缓存区中。 生产者在进行“生产”动作后，状态由P1转变为P2；而在“写”动作后，状态由P2恢复为P1。消费者进程能读取消息，并把消息从缓存器中取走。消费者在“读”动作后，状态由C1转变为C2；而在进行“消费”动作后，状态由C2恢复为C1。如果缓存器是满的，那么生产者进程必须等待，直到消费者进程从缓存器中取出一个消息，使缓存器产生一个消息空位。同样，如果缓存器是空的，那么消费者进程就必须等待，直到生产者进程产生一个消息并把所产生的消息写入缓存器中。缓存器在进行“读”动作后，缓存器大小减“1”，而在“写”动作后，缓存器大小加“1”。,25,（3） 生产者-消费者问题,三个有限状态机 M1 = (P1, P2, 写, 生产, 1, P1) 、M2 = (C1, C2, 读, 消费, 2, C1) 、M3 = (0, 1, 2, 读, 写, 3, 0)，显然，1 3 读，2 3 写。三个有限状态机的同步积复合M = M1 M2 M3，其中， Q = Q1Q2Q3； = 1 23； q0 = (q10, q20, q30) Q1Q2Q3； (q1, q2, q3), a) = (q1, q2, q3) 1(q1, a,)=q1，2(q2, a,)=q2，3(q3, a,)=q3，a 1 23 (q1, q2, q3) 1(q1, a,)=q1，2(q2, a,)=q2，a 1 2，a 3 (q1, q2, q3) 1(q1, a,)=q1，3(q3, a,)=q3，a 1 3，a 2 (q1, q2, q3) 2(q2, a,)=q2，3(q3, a,)=q3，a 2 3，a 1 (q1, q2, q3 ) 1(q1, a,)=q1，a 1，a 2，a 3 (q1, q2, q3 ) 2(q2, a,)=q2，a 2，a 1，a 3 (q1, q2, q3 ) 3(q3, a,)=q3，a 3，a 1，a 2 无定义 其余,（3） 生产者-消费者问题,27,（3） 生产者-消费者问题II (略）,课堂练习：生产者消费者系统II包含两个生产者和一个消费者。生产者进程产生消息，并等待消费者消费。 生产者在进行“生产”动作后，状态由P1转变为P2；而在“写”动作后，状态由P2恢复为P1。消费者进程能读取消息，消费者在“读”动作后，状态由C1转变为C2；而在进行“消费”动作后，状态由C2恢复为C1。生产者进程在产生一个消息后必须等待，直到消费者进程取出所产生的消息。同样，如果没有生产者进程产生的消息，那么消费者进程就必须等待，直到生产者进程产生一个消息。类似问题：生产者消费者系统包含两个生产者、一个消费者和1个缓存容量的缓存单元？生产者消费者系统包含m个生产者、n个消费者和b个缓存容量的缓存单元？,（3） 生产者-消费者问题II,29,有限状态机的缺陷,在多有限状态机系统中，系统的状态为所有状态机的状态的笛卡儿（同步、异步）积，因此系统的状态数具有状态组合复杂性问题。即使对于非常简单的情况，复合后系统的状态图的规模也会变得非常庞大，甚至无法进行；有限状态机模型实质上存在一个限制性假定：在系统所处的每一个状态上，在任何时刻，最多执行一个操作。因此，有限状态机仅能够描述顺序系统，无并发描述的能力；有限状态机不能描述无限状态系统，同时，缺乏描述时间特性的机制。有限状态机也不适合于描述系统的功能和结构特性。,30,（二） Statecharts,（1） Statecharts中的状态 Statecharts是由以色列的Harel于1987年建立的传统有限状态机的一种扩展形式。Statecharts中通过引入状态的递阶（层次化）、状态的“与（AND）”分解和“或（OR）”分解等高级特性，从而具有了更强的描述能力。Statecharts中状态用圆角方框图示，状态名标注在圆角方框内的上方 。,31, 状态的层次化,有限状态机在输入F下均可从状态S或T转移到状态U。这里可将状态S和T合并成一个新的状态，记为状态V，并将两个状态转移弧用一个弧来代替。状态的层次化通过框图的嵌套来图示。具有子状态的状态称为递阶状态，没有子状态的状态称为简单状态或者原子状态。高级状态或超状态、父状态、先辈状态、子状态、后代状态（任意深度多层次描述）,32, 或（OR）状态、与（AND）状态,状态的层次化可以通过自顶向下的状态分解，或自底向上的状态合并来实现。或（OR）状态：当且仅当位于该状态就是位于其中的一个子状态，即，位于一个或状态不能同时位于该状态的两个以上的子状态。或状态表示了子状态之间的一种异或关系。状态的或状态表示，称为状态的或分解。与（AND）状态：当且仅当位于该状态就是同时位于其所有的子状态。与状态表示了子状态之间的一种与关系。状态的与状态表示，称为状态的正交分解；与状态的子状态，又称为状态的正交分量。图形表示中，用虚线将与状态的正交分量或子状态进行隔离，与状态的标识符（即，状态名）标注在和状态边框连在一体的小方框内。,33,（2） Statecharts中的迁移,迁移上的条件、事件和动作迁移的输入称为触发（trigger），触发可以是事件或者（和）条件。迁移的输出称为动作（action），动作可以是产生新的事件或执行一个过程或函数等。输入是状态之间迁移发生的原因，只有当一个迁移的输入事件出现或者（和）迁移的输入中条件满足时，该迁移所联系的状态才可发生转移。动作的执行被认为是瞬时的。触发和动作以“事件条件/动作”的形式标注在迁移弧旁。,34, 迁移上的条件、事件和动作,预定义的与状态、数据项、时间有关的条件、事件和动作 （P36） 条件：in(S) 表示是否处于状态S中，如是则为真，否则为假； ac(A) 表示活动A是否处于活动状态，如是则为真，否则为假； hg(A) 表示活动A是否处于挂起状态，如是则为真，否则为假；事件：en(S) 表示进入状态S；ex(S) 表示退出状态S；ns表示正在进入当前状态； xs表示正在退出当前状态；st(A)表示活动A被启动；st表示当前活动被启动；sp(A)表示活动A被停止；tr(C)表示条件C变为真；fs(C)表示条件C变为假；rd(X)表示X被动作rd!读；wr(X)表示X被动作wr!写；ch(X)表示数据项X的值发生改变；tm(E，N)表示事件E发生后，已过了N个时间单位。动作：tr!(C) 表示对条件C赋值真；fs!(C) 表示对条件C赋值假；st!(A)表示启动活动A；sp!(A)表示停止活动A；sd!(A)表示挂起活动A；rs!(A)表示重新开始活动A；rd!(X) 表示读数据或条件X；wr!(X) 表示写数据或条件X；hc!(S) 表示忘记状态S的历史信息；hd!(S) 表示忘记状态S的后继状态的历史信息。事件、条件和动作可进行逻辑and ,or ,not等运算。如：E1 and E2表示事件E1与E2同时发生；C1 or C2表示C1和C2的或逻辑运算。, 迁移与状态的连接,迁移描述了简单状态和简单状态、简单状态和递阶状态、递阶状态和递阶状态之间的状态转移关系。迁移用有向弧图示，有向弧可以从一个状态的边界引出，终止于另一状态的边界，也可以穿过先辈状态的边界。当一个迁移没有指明其源状态时，则称之为缺省迁移。其所指向的状态，称为缺省状态。缺省迁移用圆点箭线弧表示。缺省迁移可以指向一个状态，也可以穿过先辈状态的边框直接指向某一子状态。当迁移指向一个与状态时，则相当于指向其所有的子状态；当迁移指向一个或状态时，则相当于指向其缺省的子状态。当退出一个状态时，则相当退出其所有的子状态。,36, 复合迁移,为了简化图形中迁移的有向弧线，Statecharts中引入了一些辅助符号，从而得到状态之间转移关系的复合迁移。条件连接符 也称为C-连接符，用于条件的连接。Statecharts规定始于C-连接符的条件分支可以多个，但是这些条件分支必须是异或的。,37, 复合迁移 -开关连接符,开关连接符，也称为S-连接符，用于事件的连接。,38, 复合迁移-分叉（汇合）连接符,迁移的触发和（或）动作的相同部分，可以通过分叉（汇合）连接符形成一个单一的弧线进入（离开）连接符。分叉（汇合）连接符适用于条件连接符和开关连接符所不能描述的情形。,等价 Statecharts图？,39, 复合迁移 -分叉（汇合）结构,分叉（汇合）结构是进入（离开）与状态的子状态迁移的一种描述方式。此类结构下复合迁移所联系的状态转移，要求迁移上所有的触发同时满足，且动作也都同时执行。,40, 复合迁移 -图形连接符,图形连接符可以实现迁移的异地连接。用椭圆符号并标注相同的名称来图示。Statecharts规定每个图形连接符出现与所连接的迁移必须具有相同方向的弧线（离开或者进入）。,41, 复合迁移 -历史连接符,历史连接符规定系统进入一个状态组中的一个最近访问历史状态,用标注H的圆圈图示。历史连接符可以理解为一个特殊的状态。进入历史连接符就表示进入该连接符所在状态组中最近访问的那个状态，若历史状态为空，则进入历史连接符所指向的状态。,从状态T进入状态S时，首先进入其历史状态H，即进入最近访问的那个状态。若上次访问的状态为S2，则进入状态S2。如果H为空，则进入S1状态。,42,（3） 电梯控制系统,考虑一个m层的大楼、n个电梯的服务系统。需要建立一个用以描述电梯在楼层之间的运动,并完成电梯控制系统开发的规格，系统存在如下一些约束和要求： 每个电梯内部都有一组按钮，每个按钮用于指示一个楼层。当按下某个按钮后，该按钮指示灯就会发亮，直到到达相应的楼层后按钮的指示灯自动熄灭；,43,电梯控制系统, 除了最高层和最低层以外，每个楼层都有两个按钮：一个用于请求电梯向下移动，一个用于请求电梯向上移动。这些按钮在被按下后，相应指示灯就会发亮。当电梯按照所请求的方向移动离开该楼层时，按钮的指示灯自动熄灭； 在没有服务请求时，电梯停留在其当前所处于的楼层，并且电梯门关闭。 整个电梯控制系统可分为：电梯控制按钮、楼层控制按钮和电梯运动系统三个部分。,44,电梯控制按钮,描述电梯按钮、按钮状态以及状态转换的符号定义如下：ebij 电梯i中对应于楼层j的按钮；ebonij ebij的指示灯为亮的状态；eboffij eb ij的指示灯为熄灭的状态；press_ebij ebij被按下时所产生的事件；arrives_atij 电梯i到达楼层j时所产生的事件。,45,楼层控制按钮,除了最底层和最高层以外，其它各楼层都有两个按钮：一个用于请求电梯向上运动，另一个用于请求电梯向下运动。用以描述的相应符号为：fbbj 楼层j对应于运动方向b的按钮（b up down）；fbonbj fbbj的指示灯为亮的状态；fboffbj fbbj的指示灯为熄灭的状态；call_fbbj 在fbbj被按下时所产生的事件；depart_atbj 在方向b上运动的电梯离开楼层j时所产生的事件。,46,电梯运动系统,某个楼层j所能观察到的电梯运动有如下可能的几种情形：电梯一直向上移动；电梯一直向下移动；电梯从下面往上逐渐靠近，停止，然后继续向上运动；电梯从上面往下逐渐靠近，停止，然后继续向下运动；电梯从下面往上逐渐靠近，停止，然后反向向下运动；电梯从上面往下逐渐靠近，停止，然后反向向上运动；电梯从下面往上逐渐靠近，停止，然后在空闲状态等待；电梯从上面往下逐渐靠近，停止，然后在空闲状态等待；从空闲状态起动，然后向下运动；从空闲状态起动，然后向上运动。,电梯运动系统,对于某楼层的观察者，电梯可能会处于如下状态之一：等待(w:wait)：在该层等待，并且门未打开；停止-空闲(s-i:stop-idle)：停在该层，并且门打开；停止-向上(s-u:stop-up)：电梯在向上运动过程中在该楼层暂停；停止-向下(s-d:stop-down)：电梯在向下运动过程中在该楼层暂停；靠近-向上(a-u:approach-up)：电梯在向上运动过程中逐渐靠近该楼层；靠近-向下(a-d:approach-down)：电梯在向下运动过程中逐渐靠近该楼层；退出-向上(e-u:exit-up)：电梯离开该楼层，继续向上运动；退出-向下(e-d:exit-down)：电梯离开该楼层，继续向下运动。,电梯运动系统Statecharts规格,状态s-u、s-d和s-i可以合并为一个超状态stop；状态a-u和a-d合并为超状态approach；状态e-u和e-d合并为超状态exit。电梯经过在某楼层的暂停后，将合上门然后离开该楼层，这一过程规格为状态stop在触发事件close-door下转移到状态exit。当存在某楼层对电梯的请求，并且此时的电梯正处于状态wait时，电梯将离开状态wait。这一过程规格为：在触发事件call-fb(-,-)下，状态 wait转移到状态stop.,对电梯运动过程进行如下假定：电梯在向上运动过程中，在进入状态s-u之前要经过状态a-u；同理，电梯在向下运动过程中，在进入状态s-d之前要经过状态a-d。这一转换过程，在实际电梯系统运行中需要对电梯进行减速，用reduce-speed来表示所相应的内部事件。,楼层观测到的电梯运动情况完全规格,从超状态approach到超状态stop、或者从超状态stop到超状态exit的转换并没有在前图中明确指出。为此，需要对该规格进行细化，标记出与所有子状态相关的迁移。当电梯处于状态stop-idle时，如果发生某个用户对电梯进行请求，则转移到状态stop-up或stop-down；如果没有使用请求，则电梯将进入状态wait。这一过程通过迁移called_from_up、called_from_down、change_direction、和no_request等来描述,50,状态stop-up和stop-down的细化,对状态stop_up和stop-down进行细化，以描述电梯的开关门情况,51,4个楼层和1个电梯的电梯运动系统规格,a-u: approach-up a-d: approach-down e-u: exit-up e-d: exit-down s-u: stop-up s-d: stop-downs-i: stop-idle w: wait,