3.1.3　基于有限状态机和时间自动机模型

状态机是描述系统状态与状态转换的一种形式化方法，通常由状态、转换、事件、活动和动作等部分组成，利用状态机可以精确地描述对象的行为。在计算机科学中，状态机的使用非常普遍，尤其是在通信协议及嵌入式软件的建模及验证领域。

由于实时嵌入式软件大多基于状态，而有限状态机（FSM）模型用触发事件和状态迁移描述系统的行为，因此适用于一般实时嵌入式软件的开发和测试的形式化描述。此外，为了增强有限状态机的描述能力，简化描述，使各状态之间的变化清晰化，最终提高对局部以致整个模型的描述与分析能力，出现了众多基于有限状态机的扩展方法，如CFSM（Communicating FSM）、EFSM（Extended FSM）、CEFSM（Communicating EFSM）、PFSM（Probability FSM）等。此外，基于FSM的时间自动机（Timed Automata，TA）也取得了较多的研究成果。

基于有限状态机的测试模型假设软件在某个时刻总是处于某个状态，并且当前状态决定了软件可能的输入，而且从该状态向其他状态的迁移取决于当前的输入。有限状态机模型适用于把测试数据表达为输入序列的测试方法，并可以利用图的遍历算法自动生成测试序列。

有限状态机可以用状态迁移图或状态迁移矩阵表示，可以根据状态覆盖或迁移覆盖生成测试用例。有限状态机模型有成熟的理论基础，并且可以利用形式化语言和自动机理论来设计、操纵和分析，适合描述反应式系统。早期基于FSM的经典软件测试方法包括T方法、U方法、D方法和W方法等。随着FSM技术的不断发展，逐渐出现了基于扩展的有限状态机的测试方法，如基于EFSM的测试输入数据自动选取方法，该方法通过区间削减和分段梯度最优下降算法自动选取测试输入所需的测试数据，从而代替手工选取测试数据的工作，提高测试效率，大大降低软件测试过程中的花费。EFSM比FSM能够更加精确地刻画软件系统的行为，但由于扩展有限状态机中的迁移存在前置条件，单纯地将基于有限状态机的测试方法用于扩展有限状态机会产生很多问题，如测试序列不可执行、存在不确定性等问题。

TA是在传统FSM基础上为迁移添加时钟约束，为状态添加不变式约束而得到的，添加到迁移上的时钟约束表示只有在此约束被满足时迁移才被激活，而添加到状态上的不变式约束表示只有在此不变式被满足时系统才能停留在此状态。一种基于时间自动机的实时系统测试方法如下：将时间安全输入/输出自动机描述的系统模型转换为不含抽象时间延迟迁移的稳定符号状态迁移图，然后采用基于标号迁移系统的测试方法来静态生成满足各种结构覆盖标准的迁移动作序列。最后，给出根据迁移动作序列构造和执行测试用例的过程，该过程引入了时间延迟变量目标函数，并采用线性约束求解方法动态求解迁移动作序列中的时间延迟变量。 KJyb6bbGlVVlDmT2vdlbrcYQqKeqlcRNNLc44NmNp4aN7Uktx5nqkA+xnDoPcrul