有限状态自动机，简称状态机，是一种表示有限多个状态以及在这些状态之间转移和动作的数学模型。状态用于存储关于过去的信息，它反映了从系统开始到现在时刻输入的变化；转移用于指示状态变更，用必须满足使转移发生的条件来描述它；动作是指在给定时刻要进行的活动描述。有限状态自动机中的动作类型主要包括如下几种：
（1）进入动作：在进入状态时进行。
（2）退出动作：在退出状态时进行。
（3）输入动作：依赖于当前状态和输入条件进行。
（4）转移动作：在进行特定转移时进行。
在利用有限状态机模型验证协议的正确性时，每个协议机（即发送方或接收方）在任何一个时刻，总会处于某一种特定的状态，而对于每一种状态，当某个事件发生时，状态转换就会发生，同时，会有0个或多个可能的状态转换（Transition，也称为状态变迁）来使得协议机到达其他的状态。图3.17给出了选择性重传协议的有限状态机模型，其中，每种状态由3个字符S-R-C表示，其含义分别如下：
◆ S为0或1，对应于发送方正在或试图发送的那一帧，其中，S=0表示发送了第0号帧、S=1表示发送了第1号帧。
◆ R为0或1，对应于接收方期望接收的那一帧，其中，R=0表示期待接收第0号帧、R=1表示期待接收第1号帧。
◆ C为0、1、A或空（−），对应于信道的状态，其中，C=0表示第0号帧在信道上，C=1表示第1号帧在信道上，C=‘A’表示确认帧在信道上，而C=‘−’则表示没有帧在信道上。
基于上述状态表示方法，图3.18中的状态变迁过程可描述如下：
（1）有限状态机的初始状态为（S-R-C）=（000）：表示在初始阶段，发送方发送了0号帧（S=0）、接收方期望接收0号帧（R=0），而且0号帧当前正在信道上（C=0，表示0号帧还未被接收方处理，即接收方还未对0号帧进行确认）。
（2）当变迁1发生时（图3.18（b）给出了9种可能的变迁），即接收方正确地收到了0号帧，则接收方将期望接下来能够接收到1号帧（R=1），并且还将回送对0号帧的确认帧A给发送方。因此，有限状态机的状态变为（01 A），即发送方发送了0号帧、接收方期望接收1号帧，而且0号帧的确认帧A当前正在信道上。
图3.18 选择性重传协议的有限状态机模型
（3）当变迁2发生时，即接收方正确地收到了对0号帧的确认帧A，则发送方接下来将发送1号帧。因此，有限状态机的状态变为（111），即发送方发送了1号帧、接收方期望接收1号帧，而且1号帧当前正在信道上。
（4）在正常的操作过程中，变迁1、2、3、4顺序地不断重复。在每轮循环中，两个分组（0号帧、1号帧）被依次递交，从而将发送方带回初始状态（000），即发送方试图发送序号为0的一个新帧。
（5）若发送方发送的0号帧丢失（对应变迁0），则有限状态机的状态将从（000）变迁为（00−），最终发送方超时（对应变迁7），从而有限状态机的状态将会重新变回到（000）。
（6）若接收方发送的0号帧的确认帧丢失（对应变迁0），则有限状态机的状态将从（01 A）变迁为（01−），最终发送方超时（对应变迁7），将重新发送0号帧，则有限状态机的状态将变迁为（010）；若0号帧丢失（对应变迁0），则有限状态机的状态将变迁为（01−）；若信道正确地将0号帧递交给接收方（对应变迁5），则有限状态机的状态将变迁为（01 A）。
免责声明：以上内容源自网络，版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。
