有限状态机及其扩展

1（一）有限状态机（1）

基本概念

有限状态机（finitestatemachine）或有限自动机（finiteautomata）是有限计算的基本模型，是许多形式化规格、验证方法的基础模型。

超级商场的自动门控制器自动门的前、后分别有两个缓冲区。自动门的前缓冲区用来检测是否有人接近。自动门的后缓冲区，使得控制器把门打开足够长的时间让人走进去，并且不让门在打开的时候碰到站在它附近的人。自动门控制器依据前缓冲区、后缓冲区的检测信息给出打开或闭合的动作指令。自动门的动作控制应满足如下要求（规格）：①当前缓冲区和后缓冲区均无顾客出现，则自动门处于闭合状态；②当后缓冲区有顾客出现，则自动门维持其原有状态；③当前缓冲区有顾客且后缓冲区无顾客，则打开自动门。前缓冲区后缓冲区第1页/共51页第一页，共52页。（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=frontrear：前、后缓冲区都有顾客；neither=frontrear：前、后缓冲区都无顾客closedopenfrontneitherboth,rear,neitherboth,rear,front前缓冲区后缓冲区第2页/共51页第二页，共52页。3（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)=101dec2incincincdecdecinc：增加1dec：减少1第3页/共51页第三页，共52页。4（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)=1ABCACAAABCABA12A3B,CB,CCBA4A第4页/共51页第四页，共52页。5（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是初始状态，有限状态机由此状态开始接收输入；⑤

FQ是终结状态集合，有限状态机在达到终结态后不再接收输入。

第5页/共51页第五页，共52页。6（1）

基本概念一个有限状态机包括：一个有限状态集，用于描述系统中的不同状态；一个输入符号集，用于表征系统所接收的不同输入信息；一个状态转移函数，用于表述系统在接收不同输入下,从一个状态转移到另外一个状态的规则。

状态转移函数:刻画其行为的最关键部分,一个从Q到Q的二元函数。状态转移函数通常可以用关系矩阵、状态转移表或状态转移图的形式来表示。有限状态机可用四元组M=(Q,,,q0)或三元组M=(Q,,)来表示。第6页/共51页第六页，共52页。7（1）

基本概念

状态转移矩阵

用行表示状态机所处的当前状态，列表示将要到达的下一个状态，行列交叉处表示输入字符。称该矩阵为转移函数的关系矩阵，或者有限状态机M的状态转移矩阵。模3计数器

0120incdec2incdec1decinc状态转移矩阵第7页/共51页第七页，共52页。8

状态转移表

用表格的行表示状态机所处的当前状态，列表示当前的输入字符，行列交叉处表示要到达的下一个状态。称该表格为M的状态转换表。模3计数器

输入字符状态incdec120120012状态转移表第8页/共51页第八页，共52页。9状态转移图

用圆圈（结点）表示状态；将存在转移关系的状态用有向弧连接，并标注相应的输入字符在有向弧旁；用标有箭头的结点表示初始状态；属于终结状态集中的状态用双圈表示。

01dec2incincincdecdec状态转移图模3计数器

第9页/共51页第九页，共52页。10（1）

基本概念前面讨论的有限状态机，可以看作仅接受输入符号并发生状态改变，但无任何输出的自动机器。现实生活中的许多有限状态系统,对于不同的输入信号，除内部状态不断改变外，还不断向系统外部输出各种信号。将有限状态机进行推广，引出具有输出机制的自动机器模型。带输出的自动机器模型，按照输出的不同分成两类：输出与状态有关—Moore机；输出与状态和输入有关—Mealy机。

第10页/共51页第十页，共52页。11（1）

基本概念Moore机形式定义为六元组M=(Q,,,,,q0)，其中①Q={q0,q1,…,qn}是有限状态集合；②

={1,2,…,m}是有限输入字符集合；③

={a1,a2,…,ar}是有限输出字符集合；④：Q

Q是状态转移函数；⑤：Q

是输出函数；⑥q0

Q是初始状态。

1/10/01/20/11/00/2q0q2q1例：模3余数Q={q0，q1，q2}={0，1}(qj)=j,j=0,1,2在输入010100下，输出为012212第11页/共51页第十一页，共52页。12（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下，输出为nnyny1/y0/n1/n0/y0/n1/nq0q2q1第12页/共51页第十二页，共52页。13（1）

基本概念身份认证系统（具有条件和变量机制的有限状态机）(最大允许错误次数为3)（err：报警状态；ctr：计数变量）X[con]/Y[exec]含义在于：所标注的状态转移关系在输入x且条件con成立下，转移至下一状态，并输出y且执行exec。标注中的各项x、[con]、y或[exec]可以缺省。12A3B,C[ctr<3]/[ctr:=ctr+1]BA4errC[ctr<3]/[ctr:=ctr+1]B,C[ctr=3]/[ctr:=ctr+1]B,C[ctr=3]/[ctr:=ctr+1]A,C[ctr=3]/[ctr:=ctr+1]B,C[ctr<3]/[ctr:=ctr+1]A[ctr<3]/[ctr:=ctr+1]/ctr:=0第13页/共51页第十三页，共52页。14（1）

基本概念身份认证系统err12A3BA4ctr=2ctr=2ctr=2ctr=212A3BA4ctr=3ctr=3ctr=3ctr=312A3BA4ctr=1ctr=1ctr=1ctr=112A3BA4ctr=0ctr=0ctr=0ctr=0ctr=4B,CB,CB,CB,CB,CB,CB,CB,CA,CCCCAAA第14页/共51页第十四页，共52页。15（2）

有限状态机的复合通常，软件系统是以模块或子系统的形式出现整个软件系统的有限状态机规格,需要对各个模块的有限状态机进行复合。有限状态机复合的最简单方式是笛卡尔积有限状态机的笛卡尔积复合,规格了多个有限状态机相互独立运行的行为。软件系统之间存在交互问题，有限状态机的复合也必然涉及交互问题。第15页/共51页第十五页，共52页。16（2）

有限状态机的复合有限状态机M1=(Q1,1,1,q10)和M2=(Q2,2,2,q20)

的笛卡尔积为M=M1M2=(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

无定义其余

第16页/共51页第十六页，共52页。17（2）

有限状态机的复合01dec2incincincdecdec模3计数器模4计数器01dec2incincdec3incincdecdecdec模3和模4计数器的笛卡尔积复合有3×4=12个状态每个状态下，两个模计数器均可相互独立地进行加数、减数或保持不变第17页/共51页第十七页，共52页。18（2）

有限状态机的复合每个状态有3×3=9种状态转移选择，但其中一种为无任何状态转移发生，故只有8种状态转移。其笛卡尔积复合具有12×8=96个状态转移2,02,12,32,21,01,11,31,20,00,10,30,2dec,decinc,inc,decinc,incdec,incdec,,inc,dec模计数器的笛卡尔积复合

第18页/共51页第十八页，共52页。19♣有限状态机的同步积复合有限状态机M1=(Q1,1,1,q10)和M2=(Q2,2,2,q20)

的同步积复合为M=M1M2=(Q,,,q0)，其中，

Q=Q1Q2；

=1

2

；

q0=(q10,q20)Q1Q2；((q1,q2),a)=(q1,q2)1(q1,a)=q1，2(q2,a)=q2，a12

(q1,q2)2(q2,a)=q2，a1，a2(q1,q2)1(q1,a)=q1，a1，a2

无定义其余

第19页/共51页第十九页，共52页。20♣有限状态机的同步积复合模计数器的同步积复合

2,02,12,32,21,01,11,31,20,00,10,30,2decinc模3和模4计数器，可以进行耦合运行，阻止各自的独立运行行为。

只有inc、inc和dec、dec两种共24个状态转移第20页/共51页第二十页，共52页。21♣有限状态机的异步积复合有限状态机M1=(Q1,1,1,q10)和M2=(Q2,2,2,q20)

的异步积复合为M=M1M2=(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

无定义其余第21页/共51页第二十一页，共52页。22♣有限状态机的异步积复合模计数器的异步积复合

2,02,12,32,21,01,11,31,20,00,10,30,2incdecincdec模3和模4计数器，可以进行耦合运行，但在任何状态下仅有其中一个模计数器运行。

分别有inc和dec两种共48个状态转移第22页/共51页第二十二页，共52页。（3）

生产者-消费者问题

生产者－消费者系统包含一个生产者和一个消费者。生产者进程产生消息，并把产生的消息写入一个能容纳两个消息的缓存区中。

生产者在进行“生产”动作后，状态由P1转变为P2；而在“写”动作后，状态由P2恢复为P1。消费者进程能读取消息，并把消息从缓存器中取走。消费者在“读”动作后，状态由C1转变为C2；而在进行“消费”动作后，状态由C2恢复为C1。如果缓存器是满的，那么生产者进程必须等待，直到消费者进程从缓存器中取出一个消息，使缓存器产生一个消息空位。同样，如果缓存器是空的，那么消费者进程就必须等待，直到生产者进程产生一个消息并把所产生的消息写入缓存器中。缓存器在进行“读”动作后，缓存器大小减“1”，而在“写”动作后，缓存器大小加“1”。

生产者P1生产P2写C1读C2消费读20读1写写缓存器消费者第23页/共51页第二十三页，共52页。24（3）

生产者-消费者问题

三个有限状态机M1=({P1,P2},{写,生产},1,P1)、M2=({C1,C2},{读,消费},2,C1)、M3=({0,1,2},{读,写},3,0)，显然，1

3{读}，2

3{写}。三个有限状态机的同步积复合M=M1M2M3，其中，

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，a1

23(q1,q2,q3)1(q1,a,)=q1，2(q2,a,)=q2，a1

2，a3(q1,q2,q3)1(q1,a,)=q1，3(q3,a,)=q3，a1

3，a2(q1,q2,q3)2(q2,a,)=q2，3(q3,a,)=q3，a2

3，a1(q1,q2,q3)1(q1,a,)=q1，a1，a2，a3(q1,q2,q3)2(q2,a,)=q2，a2，a1，a3(q1,q2,q3

)3(q3,a,)=q3，a3，a1，a2

无定义其余第24页/共51页第二十四页，共52页。（3）

生产者-消费者问题写生产读0,P1,C1

消费1,P1,C1

0,P1,C2

2,P1,C1

2,P1,C2

1,P1,C2

消费消费读读0,P2,C1

消费1,P2,C1

0,P2,C2

2,P2,C1

2,P2,C2

1,P2,C2

消费消费读生产生产生产生产生产写写写生产者P1生产P2写C1读C2消费读20读1写写缓存器消费者第25页/共51页第二十五页，共52页。26（3）

生产者-消费者问题II(略）

课堂练习：生产者－消费者系统II包含两个生产者和一个消费者。生产者进程产生消息，并等待消费者消费。

生产者在进行“生产”动作后，状态由P1转变为P2；而在“写”动作后，状态由P2恢复为P1。消费者进程能读取消息，消费者在“读”动作后，状态由C1转变为C2；而在进行“消费”动作后，状态由C2恢复为C1。生产者进程在产生一个消息后必须等待，直到消费者进程取出所产生的消息。同样，如果没有生产者进程产生的消息，那么消费者进程就必须等待，直到生产者进程产生一个消息。

类似问题：生产者－消费者系统包含两个生产者、一个消费者和1个缓存容量的缓存单元？

生产者－消费者系统包含m个生产者、n个消费者和b个缓存容量的缓存单元？第26页/共51页第二十六页，共52页。（3）

生产者-消费者问题II生产者1P11生产1P12写1C1读C2消费消费者生产者2P21生产2P22写2P11,P21,C1

P11,P22,C1P11,P21,C2P11,P22,C2消费消费P12,P21,C1消费P12,P22,C1P12,P21,C2P12,P22,C2消费生产1生产1生产2<写1,读>生产2生产1<写2,读>生产2生产1生产2<写2,读><写1,读>第27页/共51页第二十七页，共52页。28★有限状态机的缺陷在多有限状态机系统中，系统的状态为所有状态机的状态的笛卡儿（同步、异步）积，因此系统的状态数具有状态组合复杂性问题。即使对于非常简单的情况，复合后系统的状态图的规模也会变得非常庞大，甚至无法进行；有限状态机模型实质上存在一个限制性假定：在系统所处的每一个状态上，在任何时刻，最多执行一个操作。因此，有限状态机仅能够描述顺序系统，无并发描述的能力；有限状态机不能描述无限状态系统，同时，缺乏描述时间特性的机制。有限状态机也不适合于描述系统的功能和结构特性。

第28页/共51页第二十八页，共52页。29（二）Statecharts（1）

Statecharts中的状态

Statecharts是由以色列的Harel于1987年建立的传统有限状态机的一种扩展形式。Statecharts中通过引入状态的递阶（层次化）、状态的“与（AND）”分解和“或（OR）”分解等高级特性，从而具有了更强的描述能力。Statecharts中状态用圆角方框图示，状态名标注在圆角方框内的上方。SS2S22S21S1S1FFS3S2T1TSUT2第29页/共51页第二十九页，共52页。30①

状态的层次化

有限状态机在输入F下均可从状态S或T转移到状态U。这里可将状态S和T合并成一个新的状态，记为状态V，并将两个状态转移弧用一个弧来代替。状态的层次化通过框图的嵌套来图示。具有子状态的状态称为递阶状态，没有子状态的状态称为简单状态或者原子状态。高级状态或超状态、父状态、先辈状态、子状态、后代状态

（任意深度多层次描述）SFFUT

SVFUTSS2S22S21S1第30页/共51页第三十页，共52页。31②

或（OR）状态、与（AND）状态状态的层次化可以通过自顶向下的状态分解，或自底向上的状态合并来实现。或（OR）状态：当且仅当位于该状态就是位于其中的一个子状态，即，位于一个或状态不能同时位于该状态的两个以上的子状态。或状态表示了子状态之间的一种异或关系。状态的或状态表示，称为状态的或分解。与（AND）状态：当且仅当位于该状态就是同时位于其所有的子状态。与状态表示了子状态之间的一种与关系。状态的与状态表示，称为状态的正交分解；与状态的子状态，又称为状态的正交分量。图形表示中，用虚线将与状态的正交分量或子状态进行隔离，与状态的标识符（即，状态名）标注在和状态边框连在一体的小方框内。S1FFS3S2T1TSUT2SS2S22S21S1第31页/共51页第三十一页，共52页。32

（2）Statecharts中的迁移

迁移上的条件、事件和动作迁移的输入称为触发（trigger），触发可以是事件或者（和）条件。迁移的输出称为动作（action），动作可以是产生新的事件或执行一个过程或函数等。输入是状态之间迁移发生的原因，只有当一个迁移的输入事件出现或者（和）迁移的输入中条件满足时，该迁移所联系的状态才可发生转移。动作的执行被认为是瞬时的。触发和动作以“事件[条件]/动作”的形式标注在迁移弧旁。

S1E[in(S1)]/R[t=2]/FS3S2T1TSRT2RF/EF/R第32页/共51页第三十二页，共52页。33①迁移上的条件、事件和动作预定义的与状态、数据项、时间有关的条件、事件和动作（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等运算。如：E1andE2表示事件E1与E2同时发生；C1orC2表示C1和C2的或逻辑运算。

第33页/共51页第三十三页，共52页。②

迁移与状态的连接

迁移描述了简单状态和简单状态、简单状态和递阶状态、递阶状态和递阶状态之间的状态转移关系。迁移用有向弧图示，有向弧可以从一个状态的边界引出，终止于另一状态的边界，也可以穿过先辈状态的边界。当一个迁移没有指明其源状态时，则称之为缺省迁移。其所指向的状态，称为缺省状态。缺省迁移用圆点箭线弧表示。缺省迁移可以指向一个状态，也可以穿过先辈状态的边框直接指向某一子状态。当迁移指向一个与状态时，则相当于指向其所有的子状态；当迁移指向一个或状态时，则相当于指向其缺省的子状态。当退出一个状态时，则相当退出其所有的子状态。RFS2S22S21S1RFS2S22S21S1URFSS22S21S1TT2T1U第34页/共51页第三十四页，共52页。35

③复合迁移

为了简化图形中迁移的有向弧线，Statecharts中引入了一些辅助符号，从而得到状态之间转移关系的复合迁移。条件连接符

也称为C-连接符，用于条件的连接。Statecharts规定始于C-连接符的条件分支可以多个，但是这些条件分支必须是异或的。

S1S3S2[C1]EC[C2]S1S3S2E[C1]E[C2]第35页/共51页第三十五页，共52页。36

③复合迁移

--开关连接符

开关连接符，也称为S-连接符，用于事件的连接。S1S3S2E1ASE2E3S1S3S2AE1AE2AE3第36页/共51页第三十六页，共52页。37

③复合迁移--分叉（汇合）连接符

迁移的触发和（或）动作的相同部分，可以通过分叉（汇合）连接符形成一个单一的弧线进入（离开）连接符。分叉（汇合）连接符适用于条件连接符和开关连接符所不能描述的情形。

S1S3S2R/ASS1S3S2[C1]EFS1S3S2SETS1S3S2/A[C1]E等价Statecharts图？第37页/共51页第三十七页，共52页。38

③复合迁移--分叉（汇合）结构分叉（汇合）结构是进入（离开）与状态的子状态迁移的一种描述方式。此类结构下复合迁移所联系的状态转移，要求迁移上所有的触发同时满足，且动作也都同时执行。

US1S3SS2S4AE1/A1[c2]/A2US1S3SS2S4A[c1]/A1E2/A2第38页/共51页第三十八页，共52页。39

③复合迁移--图形连接符

图形连接符可以实现迁移的异地连接。用椭圆符号并标注相同的名称来图示。Statecharts规定每个图形连接符出现与所连接的迁移必须具有相同方向的弧线（离开或者进入）。

S1INTSS2S3A[E1]/A1INTRINT第39页/共51页第三十九页，共52页。40

③复合迁移--历史连接符

历史连接符规定系统进入一个状态组中的一个最近访问历史状态,用标注H的圆圈图示。历史连接符可以理解为一个特殊的状态。进入历史连接符就表示进入该连接符所在状态组中最近访问的那个状态，若历史状态为空，则进入历史连接符所指向的状态。

S1HS2TS从状态T进入状态S时，首先进入其历史状态H，即进入最近访问的那个状态。若上次访问的状态为S2，则进入状态S2。如果H为空，则进入S1状态。第40页/共51页第四十页，共52页。41

（3）电梯控制系统考虑一个m层的大楼、n个电梯的服务系统。需要建立一个用以描述电梯在楼层之间的运动,并完成电梯控制系统开发的规格，系统存在如下一些约束和要求：①

每个电梯内部都有一组按钮，每个按钮用于指示一个楼层。当按下某个按钮后，该按钮指示灯就会发亮，直到到达相应的楼层后按钮的指示灯自动熄灭；第41页/共51页第四十一页，共52页。42

电梯控制系统②

除了最高层和最低层以外，每个楼层都有两个按钮：一个用于请求电梯向下移动，一个用于请求电梯向上移动。这些按钮在被按下后，相应指示灯就会发亮。当电梯按照所请求的方向移动离开该楼层时，按钮的指示灯自动熄灭；③在没有服务请求时，电梯停留在其当前所处于的楼层，并且电梯门关闭。

整个电梯控制系统可分为：电梯控制按钮、楼层控制按钮和电梯运动系统三个部分。第42页/共51页第四十二页，共52页。43

电梯控制按钮描述电梯按钮、按钮状态以及状态转换的符号定义如下：ebij

电梯i中对应于楼层j的按钮；ebonij

ebij的指示灯为亮的状态；eboffijebij的指示灯为熄灭的状态；press_ebij

ebij被按下时所产生的事件；arrives_atij

电梯i到达楼层j时所产生的事件。

ebonijeboffijarrives-atijpress-ebij第43页/共51页第四十三页，共52页。44

楼层控制按钮除了最底层和最高层以外，其它各楼层都有两个按钮：一个用于请求电梯向上运动，另一个用于请求电梯向下运动。用以描述的相应符号为：fbbj

楼层j对应于运动方向b的按钮（b

{updown}）；fbonbj

fbbj的指示灯为亮的状态；fboffbj

fbbj的指示灯为熄灭的状态；call_fbbj

在fbbj被按下时所产生的事件；depart_atbj

在方向b上运动的电梯离开楼层j时所产生的事件。

fbonbjfboffbjcall-fbbjdepart-atbj第44页/共51页第四十四页，共52页。45

电梯运动系统某个楼层j所能观察到的电梯运动有如下可能的几种情形：电梯一直向上移动；电梯一直向下移动；电梯从下面往上逐渐靠近，停止，然后继续向上运动；电梯从上面往下逐渐靠近，停止，然后继续向下运动；电梯从下面往上逐渐靠近，停止，然后反向向下运动；电梯从上面往下逐渐靠近，停止，然后反向向上运动；电梯从下面往上逐渐靠近，停止，然后在空闲状态等待；电梯从上面往下逐渐靠近，停止，然后在空闲状态等待；从空闲状态起动，然后向下运动；从空闲状态起动，然后向上运动。第45页/共51页第四十五页，共52页。

电梯运动系统对于某楼层的观察者，电梯可能会处于如下状态之一：等待(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)：电梯离开该楼层，继续向下运动。

e-ue-u①

e-de-d②

③

a-us-ue-ue-ds-da-d④

e-ua-d⑥

s-us-d

a-us-ue-ds-d⑤

a-us-uws-i⑦

a-d⑧

s-dws-ie-u⑨

s-uwe-ds-dw⑩

第46页/共51页第四十六页，共52页。

电梯运动系统Statecharts规格

sensorsensorexitexit-downexit-upstopstop-upstop-downstop-idlecall-fbbjclose-doorclose-doorreduce-speedwaitapproachapproach-upapproach-down状态s-u、s-d