基于状态的系统和有限状态机FSM

介绍
基于模型进行测试。模型可能是规格或描述感兴趣的属性。
该模型通常是一个抽象概念，应该相对容易理解。
测试补充了白盒方法。
测试通常是黑盒：不考虑实际系统的结构。
如果模型具有形式语义，则可实现的主要好处：我们就有了自动化的潜力。
大部分工作使用基于状态的语言 state-based languages

基于状态的系统
许多真实系统都有内部状态。
这些系统可以使用语言建模,eg 状态图。
由于它们的重要性，人们特别感兴趣针对以下领域的基于状态的测试：
(1) 交通运输（汽车、铁路、航空电子……）
(2) 机器人与自主系统
(3) 通讯协议
与许多其他系统相关

状态图是一种建模语言和一种用于描述反应式系统行为的形式主义。它提供了一种可视化表示，用于以分层和结构化的方式指定系统的状态、转换和操作。状态图对于为具有多个并发状态和复杂行为的复杂系统建模特别有用。

以下是状态图的一些主要特性和概念：

状态：状态图允许您定义系统可能处于的不同状态。状态表示系统的特定模式、条件或行为。状态可以有进入动作（进入状态时执行的动作）和退出动作（离开状态时执行的动作）。
事件：事件是导致状态之间转换的刺激或触发器。事件可以是内部的（在系统内生成）或外部的（从环境中接收）。当事件发生时，它会导致状态转换。
转换：转换定义了与响应事件而从一种状态到另一种状态的变化相关联的条件和动作。转换可以有守卫（转换发生必须满足的条件）和动作（转换期间执行的动作）。
分层状态：状态图支持状态的分层结构，允许对具有嵌套状态的复杂系统进行建模。状态可以有子状态，转换可以发生在父状态内的子状态之间或父状态之间。
正交区域：状态图还可以通过使用正交区域对并发行为进行建模。正交区域表示系统中可以同时执行的独立组件，每个组件都有自己的状态和转换。
历史状态：历史状态会记住父状态中先前处于活动状态的子状态，允许系统在重新进入父状态时恢复其先前的行为。

状态图提供系统行为的图形表示，通常使用状态图，其中状态表示为节点，转换表示为有向边。它们提供了一种清晰直观的方法来建模和分析反应式系统的行为，从而更容易理解、交流和推理复杂的系统动力学。
状态图通常用于各个领域，包括软件工程、控制系统、嵌入式系统和用户界面设计。它们得到各种建模工具和框架的支持，这些工具和框架有助于创建、模拟和验证基于状态图的模型。

状态和转换States and Transitions
系统可以通过以下方式建模：
一组逻辑状态。这些状态之间的转换。
然后：
每个逻辑状态通常代表内部变量的一些（tuples）值
每个转换都将代表一个操作的使用状态或输入/输出对。

状态和转换：嵌入式系统embedded systems
许多嵌入式控制系统的运行周期如下：
从传感器读取值（输入）
然后根据当前状态信息（内部变量的值）处理这些值。
最后，将值（输出）发送到执行器并更新内部变量的值。
因此，每个循环都涉及输入，然后是输出和状态变化。

故障Faults
可以考虑：
(1) 转换产生错误的输出（输出故障）。
(2) 转换具有错误的结束状态（状态转移错误）。
(3) 有额外的状态。
我们希望能够测试这些。通常，输出故障是最容易发现的。

有限状态机Finite State Machines
最简单的基于状态的模型，具有输入和输出。
有状态和状态之间的转换。
每个转换都有一个标签：输入/输出对。
有一个初始状态。
这本质上是一个有限自动机，其中：
所有状态都是最终状态。字母表是输入/输出对的集合。
称为 Mealy 机器。

使用 FSM
开发中使用的语言比 FSM 更丰富（例如有逻辑状态和内部状态变量）。
但是，FSM 测试生成技术经常使用（或改编）：
工具可以扩展内部状态变量。这可以是一个预处理步骤，或者“扩展”可以即时发生。
通常可以抽象出大部分日期。例如，考虑通信协议中的消息数据。

逻辑状态：逻辑状态通过合并描述系统行为或模式的附加信息或条件来扩展系统中的状态概念，而不仅仅是简单的状态转换。虽然传统的 FSM 通常将状态表示为离散的原子实体，但逻辑状态引入了复合或聚合状态的概念，以捕获更复杂的行为和条件。

逻辑状态可用于表示需要满足多个标准或约束的更高级别模式或条件。它们允许对单个状态转换无法充分捕获的复杂行为进行规范。通过引入逻辑状态，可以在更高的抽象层次上对系统行为进行建模，从而实现更灵活和更具表现力的表示。

内部状态变量：内部状态变量，也称为状态属性或变量，用于表示和跟踪与系统中的状态相关的附加信息。虽然 FSM 主要关注状态转换，但内部状态变量提供了一种机制来捕获和更新特定于状态的数据或条件。

内部状态变量可用于存储和操作与系统当前状态相关的信息，例如计数器、标志、计时器或与状态行为相关的任何其他数据。这些变量可以在状态转换期间或响应外部事件时进行修改，它们的值可以影响系统的行为或后续的状态转换。
通过合并内部状态变量，系统的建模能力得到增强，允许更细微的行为和状态相关的决策制定。内部状态变量使系统能够维护和利用特定于每个状态的信息，从而导致更复杂和上下文感知的系统行为。

有限状态机测试
测试生成算法可以利用：
有限自动机理论Finite Automata Theory：FSM 本质上是特殊类型的有限自动机，因此可以使用相应的算法和理论。
图论Graph Theory：FSM 可以看作是一个有向图, 每条边都有一个标签。因此，我们也可以使用图论结果和算法。

确定性有限状态机 deterministic finite state machine的主要特征
（确定性）有限状态机 (FSM)，也称为确定性有限自动机 (DFA)，是一种用于描述系统或过程行为的数学模型。它是一种状态机，其行为仅由当前状态和接收到的输入决定。

在确定性 FSM 中，每个状态都有一组已定义的转换，这些转换根据当前状态和正在处理的输入符号指定下一个状态。机器的行为是通过在提供输入时遵循这些转换来确定的。

以下是确定性有限状态机的主要特征：

状态：一组有限的状态表示系统可能处于的不同模式或条件。FSM 在任何给定时间只能处于一种状态。
转换：转换表示基于接收到的输入符号的状态变化。每个转换都与一个特定的状态和输入符号组合相关联，指定要转换到的下一个状态。
输入：FSM 从输入字母表中接收输入符号。这些符号触发状态转换并确定机器的行为。
确定性行为：在确定性 FSM 中，对于任何给定的当前状态和输入符号，只有一个有效的下一状态。这意味着机器的行为完全由当前状态和正在处理的输入符号决定。
接受（最终）状态：FSM 可能有一个或多个指定的接受状态，表明成功或期望的结果。当机器达到接受状态时，表示已根据定义的规则成功处理了输入。

确定性有限状态机广泛应用于计算机科学和工程的各个领域，包括形式语言理论、编译器设计、协议规范和软件建模。它们提供了一种简单而正式的方式来表示和推理系统的行为，这些系统表现出离散的、顺序的行为，并且可以使用算法和数学技术轻松实现和分析。
在这里插入图片描述

确定性Deterministic 和完全指定Completely-Specified的 FSM
FSM 是确定性的，如果：对于每个状态 s 和输入 x，至多有一个离开 s 的转换具有输入 x。
如果满足以下条件，则 FSM 是完全指定的：对于每个状态 s 和输入 x，至少存在一个离开 s 且具有输入 x 的转换。
给出的形式主义描述了 FSM 是完全指定和确定的：
如果我们想要描述不完全指定的 FSM，那么我们需要允许 δ 和 λ 是偏函数。
如果我们想描述非确定性那么我们使用S × X -> P(S × Y )替换具有转换的状态传递和输出函数（δ 和 λ）。
我们将专注于确定性和完全指定。

初始和强连接
如果满足以下条件，则 M 最初是连接的：
每个状态都可以从初始状态到达：对于每个状态 s，都有一些输入序列 x 将 M 从初始状态带到 s (δ(s0,x) = s)。

s0：它表示 FSM M 的初始状态。这是机器开始运行的状态。
x：它表示作为输入提供给 FSM 的输入序列或符号串。
δ：表示FSM的过渡函数。它以当前状态和输入符号作为参数并返回下一个状态。
s：代表FSM中的一个状态。表达式 δ(s0, x) = s 断言从初始状态 s0 开始，当处理输入序列 x 时，FSM 转换到状态 s。

简单来说，表达式 δ(s0, x) = s 意味着如果我们从初始状态 s0 开始并将输入序列 x 应用于 FSM M，则结果状态将为 s。换句话说，存在将 FSM 从初始状态带到指定状态 (s) 的输入序列 (x)。
此条件确保 FSM M 中的每个状态都可以从初始状态到达。它保证至少有一个可能的输入序列导致机器中的每个状态。此属性对于确定 FSM 的连接性很重要，可确保没有状态是不可访问或孤立的。

如果满足以下条件，则 M 是强连通的：
对于每个有序的状态对 (s,s0) 都有一些输入, 将 M 从 s 带到 s0 (δ^*(s, x) = s0) 的序列 x。

δ^*: 它表示 FSM 的扩展转移函数，它接受当前状态和输入序列作为参数，并返回最终的状态。

简单来说，表达式 δ^*(s, x) = s0 意味着如果我们从状态 s 开始，并将输入序列 x 应用于 FSM M，最终达到的状态是 s0。换句话说，存在一个输入序列（x）使得 FSM 从状态 s 经过一系列转换到达指定的状态 s0。
这个条件确保了 FSM M 是强连通的，也就是说，在 FSM 中的任意两个状态对 (s, s0) 之间，都存在一条序列 x 的输入路径，可以从状态 s 转换到状态 s0。

如果 M 最初没有连接，那么我们可以删除不可达状态。