基于时间安全输入输出自动机的测试方法及系统

摘要

本发明基于时间自动机的一种变体——时间安全输入输出自动机提出了一种实时系统测试系统和测试方法。该方法首先将时间安全输入输出自动机描述的系统模型转换为不含抽象时间延迟迁移的稳定符号状态转移图；然后采用基于输入/输出标号迁移系统的测试方法来静态生成满足各种结构覆盖标准的含时间延迟变量转移动作序列；最后，引入的时间极值函数并利用线性约束求解方法动态求解转移动作序列中的时间延迟变量以进行测试。利用本方法所实现的测试系统适用于各种带时间约束的软件系统的黑盒测试。

说明书

技术领域

本发明涉及一种时间安全输入输出自动机的测试方法，也涉及利用该测试方法实现的测试系统，属于软件测试技术领域。

背景技术

和运行环境的交互行为存在时间约束的系统称为实时系统。对于很多实时系统而言，系统的功能性错误或者对时间约束的偏移都会产生灾难性的后果。为了提高实时系统的质量，一般采用验证或测试的方法，其中，测试是唯一能够在运行时刻检验实时系统动态行为的方法。从70年代开始，研究人员就已经基于各种时间无关形式模型，如有限状态机、扩展有限状态机、标号转移系统等等，提出了许多测试用例生成方法，其中有些方法，如：U-方法、D-方法、W-方法和Wp-方法，已经在通信协议、硬件电路设计等领域得到了较为广泛的应用，但是这类方法无法描述实时系统中的时间约束。从90年代中期开始，随着时序逻辑(Temporal Logic，TL)、时间自动机(Timed Automata，TA)、时间标号迁移系统(Timed labeled Transition System，TLTS)等时间相关形式模型理论的逐步成熟，人们开始研究如何利用时间相关的形式模型来对实时系统进行测试。然而，由于实时系统引入了时间维，理论上来说其状态空间是无限的；另外，系统中的时间约束也增加了分析系统可能行为的难度，这些都给实时系统测试带来了极大的困难。

当前，有一些实时系统测试方法首先将实时系统模型转换为不含时间约束系统模型，以消除时间约束对系统行为分析造成的影响，然后使用时间无关的测试方法进行测试。然而，这些方法为了能够实现时间模型向非时间模型的转换，大多对模型的时间描述能力进行了限制；另外，尽管转换生成的时间无关模型的状态数有限，但仍然相当庞大，还需要进一步简化。

另外，为了降低状态空间爆炸给测试用例生成时带来的难度，已经存在一些系统化简方案，它们采用各种(强度不同的)时间抽象方法来对系统进行简化。这些方法基本思想均是将时间自动机中的一个位置和一个时间域一起构成一个符号状态以生成有限状态模型，其中最为典型的是域图(Region Graph)和区图(Zone Graph)。但是，区图并不适合用于测试，其主要原因是区图中的符号状态不具有稳定性属性，根据区图生成的符号状态转移序列并不一定可行，这使得采用这种方法生成测试用例的方法往往只能用于测试系统中与状态可达性相关的属性。域图生成的符号状态图虽然满足稳定性，但是该方法生成的符号状态数会随着时间自动机中时钟个数以及时间约束常数的大小而进行指数增长。利用经典的符号状态拆分方法可以获得最简稳定符号状态转移图(Minimal StableTransition Graph of Symbol State，MSTGSS)。尽管对于状态可达性分析而言，该方法生成的符号状态转移图是最简稳定的，但是对于测试而言，该方法所生成的转移图中仍然存在冗余的抽象时间延迟转移；另外，该方法的执行效率也有待改进。

由于对时间描述能力的限制以及状态化简方法不完善，目前基于时间自动机的实施系统测试工具，如COSPAN、KRONOS、UPPAAL等，普遍存在测试不充分、测试执行速度慢、难以用于复杂系统的测试等缺陷。

发明内容

因为时间安全输入输出自动机中时间变量可以取实数值，所以即使一个非常简单的时间安全输入输出自动机模型，也会存在无穷多个状态；另外，时间安全输入输出自动机的动作转移中含有时钟约束条件，只有当时钟约束条件满足时动作转移才可以进行。这种状态空间爆炸以及时钟约束条件对模型中行为的影响给测试造成了极大的困难，为此需要将时间安全输入输出自动机模型转换为更加适合测试的模型。

针对上述问题，本发明的目的在于提供一种基于时间安全输入输出自动机(TimedSafety Input/Output Automata，简称TSIOA)的测试方法，该测试方法充分利用TSIOA描述机制简单和描述能力强大的特点，通过增加预处理过程以及采用更加简洁的符号状态拆分算子等方法改进了符号状态拆分方法，并从所生成的最简稳定符号状态转移图中去除了和测试无关的抽象时间延迟转移，从而得到更加简单的不含抽象时间转移稳定符号状态转移图(Untimed Stable Transition Graph of Symbol State，简称USTGSS)；然后利用USTGSS依次生成满足各种结构覆盖标准的含时间延迟变量转移动作序列和时间测试用例，从而有效避免因为引入时间而导致的状态空间爆炸，并且能够有效的发现系统中存在的各种转移错误和时间错误。

为实现上述的发明目的，本发明所提供的基于时间安全输入输出自动机的测试方法包括以下步骤，如图1所示：

(1)建立被测系统的形式模型：所使用的建模工具是时间安全输入输出自动机，时间安全输入输出自动机模型描述了被测系统的转移关系和各种时间约束。

(2)化简形式模型：对被测系统的形式模型进行化简，采用改进的符号状态拆分算法不断递归地进行符号状态拆分，直至获得满足稳定性的符号状态集合，即，含抽象时间转移的最简稳定符号状态图。具体过程为：首先根据模型中的位置以及位置对应的时间不变量创建最初的符号状态集合；之后根据每个位置自身的时间域和从其出发的转移的约束条件来进行拆分；然后从初始符号状态出发，按照转移关系来遍历状态集，每遇到一个符号状态便利用拆分操作来判断其是否满足稳定性，如果不满足则回溯到该符号状态的紧前符号状态重新判断其稳定性，不断递归地进行符号状态拆分，直至获得满足稳定性的符号状态集合。

(3)转移去除抽象时间：对含抽象时间转移的最简稳定符号状态图(MSTGSS进行化简，采用抽象时间去除算法，将抽象时间转移从状态图中去除，从而得到不含抽象时间转移的最简稳定符号状态图。

MSTGSS中除了含有动作转移，还含有抽象的时间延迟转移。抽象的时间延迟转移表示经过了一个时间延迟，但是不能确定具体的时间量。实际上，对于符号状态图中的每一个动作转移来说，都存在相应的时间延迟转移位于动作转移之前，但是MSTGSS中只描述了那些会导致符号状态的可达性发生变化的时间延迟转移，而那些不会导致符号状态可达性发生变化的时间延迟转移则隐含在符号状态中。这种对时间延迟转移的区分对于符号状态可达性分析是有意义的，但是，由于测试执行过程中只能观察被测系统的输入、输出动作以及动作发生的时刻，而并不知道时间延迟转移是否对转移图中符号状态的可达性产生了影响；另外测试所需要的是具体的动作发生时刻，而并不是抽象的时间延迟，所以对于测试而言这种区分没有用处。为此，如果是为了测试的目的，可以将MSTGSS中的抽象时间延迟转移去除，从而对转移图进一步简化。去除了抽象时间延迟转移后得到的转移图中每一个动作转移之前都有一个隐含的时间延迟转移，故而可以在转移图中每一个转移动作之前增加一个时间变量来表示时间延迟量，并将这个时间变量与动作转移合并成新的转移标号。

(4)生成转移动作序列：根据不含抽象时间转移的最简稳定符号状态图生成可执行的含时间延迟变量的转移动作序列，转移动作序列中每两个转移动作之间均含有一个时间延迟变量。

(5)执行转移动作序列，采用动态约束求解方法，求解转移动作序列中时间延迟变量的值，具体做法是：首先根据转移动作序列建立线性约束系统，然后求解当前连续输入动作之前的时间延迟变量，并根据求得的结果执行测试，直到转移动作序列执行完毕。

(6)报告测试结果。

本发明的另一个目的在于提供一种与上述方法相对应的基于时间安全输入输出自动机的测试系统，所述的系统通过计算机软件实现。

如图2所示，基于时间安全输入输出自动机的测试系统包括系统建模器、模型转换器、转移动作生成器、测试用例生成和执行器、测试执行接口。

其中，系统建模器根据被测系统规约，对整个被测系统进行建模，所使用的建模工具是时间安全输入输出自动机(TSIOA)，测试系统主要基于TSIOA模型对被测系统进行测试。

所述的模型转换器由时间自动机化简模块和时间转移去除模块构成，用于对由系统建模器生成的TSIOA模型进行化简。首先利用时间自动机化简模块将TSIOA模型化简为最简稳定符号状态转移图(MSTGSS)，然后利用时间转移去除模块继续对MSTGSS进行化简，输出不含抽象时间延迟迁移的稳定符号状态转移图(USTGSS)。

所述的转移动作生成器根据模型转换器输出的USTGSS，利用上述的测试方法中步骤(4)所述的方法，生成可行的含时间延迟变量的转移动作序列，其中，转移动作序列中每两个转移动作之间均含有一个时间延迟变量，表示时间的迁移。

所述的测试用例生成和执行器动态求解并执行所述转移动作生成器生成的转移动作序列中的时间延迟变量，从而获得系统的时间测试用例，并通过测试执行接口来执行测试。时间测试用例生成和执行器中含有线性约束求解模块、用例生成模块和用例执行模块，其中，线性约束求解模块用于求解时间延迟量，该模块可以以多项式时间求解满足时间约束的时间延迟变量的值。为了获得更好的错误检测能力，所述线性约束求解模块在求解时间延迟变量时不仅考虑系统本身的各种时间约束，还引入了时间极值函数，从而实现各种时间延迟策略。利用线性约束求解模块求解转移动作序列中的时间延迟变量，用例生成模块便可以得到测试用例，同时，用例执行模块也可以通过测试执行接口执行所得到的测试用例。

所述时间极值函数是指TSIOA模型中使用到的各种计时器的线性表达式的极值，包括极大值和极小值，以及它们的组合情况。

所述时间延迟策略主要是指各种时间延迟量的极值，包括：转移动作序列最长、最短时间延迟，时间延迟变量最大、最小值，时间延迟变量的极值组合等。

所述测试执行接口实现所述测试管理器与所述测试用例执行器之间的连接，测试用例中所有的输入转移动作均通过测试执行接口发送给被测系统，同时，测试系统也通过测试执行接口来接收所有被测系统的输出转移动作。

本发明所实现的基于时间安全输入输出自动机的测试方法及测试系统，可以将时间测试用例中的转移动作和时间延迟量分开处理，其中前者是在不含抽象时间转移的最简稳定符号状态图基础上利用时间无关静态测试方法获得，后者通过建立线性约束系统和引入时间极值函数在测试过程中动态求解得到。利用这种方法可以根据系统的模型，很方便地生成满足各种结构覆盖和时间延迟极值覆盖标准的测试用例集合，适用于各种具有时间约束软件系统的黑盒测试。

附图说明

图1是基于时间输入输出自动机模型的测试方法流程图；

图2是基于时间输入输出自动机模型的测试系统结构示意图；

图3是实施例中一时间安全输入输出自动机模型示意图；

图4是图3中的模型经过预处理得到的符号状态集合；

图5是图4经过符号状态拆分后得到的最简稳定符号状态转移图G；

图6是图5去除了抽象时间转移后得到的不含抽象时间的最简稳定符号状态转移图。

具体实施方式

以下结合附图对本发明所提供的基于时间输入输出自动机模型的测试方法及其系统做进一步的描述，但不构成对本发明的限制。

实施例一：基于时间输入输出自动机模型的测试方法：

(1)采用时间安全输入输出自动机建立被测系统的形式模型，该模型如图3所示，该模型初始位置为I₀，时钟x和y都为0，随着时间的变化，当x大于1时，系统便可以接受动作a，并转移到位置I₁，在转移过程中将时钟y重置为0；同样，当系统位于I₁，时钟x小于3并且y大于1时，系统可以输动作c，并转移到位置I₃上。该图中位置I₀和位置I₁分别有一个时间不变量限制，表示只有x小于2，系统才可以位于I₀，只有当y小于等于2，系统才可以位于I₁。

(2)对图3所示的时间输入输出自动机模型进行化简，得到含抽象时间转移的最简稳定符号状态图。在本实施例中，该步骤是通过一种改进的符号状态拆分方法实现的，具体的算法实现如下：

(1)  ReachPartition(A){(2)  let W:＝，ρ:＝；(3)  for every l∈A.L.do(4)      W:＝W{＜Lim(l)＞}      od(5)  for every s_i∈W do(6)      ρ:＝ρ split(s_i，{e.gnard|e.source＝s_i.locatill})      od(7)  let α:＝{[s₀]}，σ:＝；(8)  while α≠σ do(9)    choose Xin ασ；(10)   let α′:＝split(X，ρ)；(11)   if α′:＝{X}then(12)      σ:＝σ∪{X}；α:＝α∪post_ρ(X)；      else(13)      α:＝α{X}；(14)      ifY∈α′such that s₀∈Y then α:＝α∪{Y}；fi(15)      σ:＝σpre_ρ(X)；(16)      ρ:＝(ρ{X})∪α′：      fi   od(17)return α；}

其中，参数A表示一个时间输入输出自动机(TSIOA)模型，ρ表示当前符号状态集，α表示可达符号状态集，σ表示当前α集合中稳定的符号状态集合。该算法中的第3-6步是预处理过程，其中第3、4步将一个TSIOA模型A的每一个位置和其时间不变量组合构成最初的符号状态集合W，第5、6步将W中的每一个符号状态根据A中与其对应的转移的条件进行拆分。从第8步开始，对符号状态集中符号状态进行拆分，如果一个可达符号状态X已经是稳定的，那么第12步将X加到σ并将其所有紧后符号状态加入σ中；否则将X移出稳定的符号状态集合α，为了避免α为空，第14步对X的拆分结果进行判断，如果存在含有初始状态的符号状态Y，则将其加入到α；第15、16步分别将X的紧前符号状态移出σ，并根据拆分结果更新当前符号状态集ρ。第10步中split拆分操作得到的符号状态集合是最简稳定的，所以最终得到的符号状态集合是最简稳定的。

本实施例中，以图3所示的时间输入输出自动机模型为参数调用上述的算法，经过算法的预处理过程可以得到了如图4所示的经过预处理获得的符号状态集合，该图中包含11个符号状态，其中每个符号状态中的位置信息表示了该符号状态是从时间自动输入输出自动机模型的哪个状态经过预处理拆分得到的。在图3所示算法的输出结果的基础上增加转移关系后，得到了图5所示的经过符号状态拆分后得到的转移图G，该图包含了10符号状态图，各个符号状态图中转移均满足稳定性要求，另外除了动作转移之外，该图还含有抽象时间转移τ，表示一个时间长度不确定的时间转移。图5所示的这种转移图称为最简稳定符号状态转移图(MSTGSS)，它是一个三元组{V，E，v0}，分别表示转移图中符号状态集合，转移集合以及初始符号状态。

(3)对含抽象时间转移的最简稳定符号状态图进行化简，得到不含抽象时间转移的最简稳定符号状态图。

在本实施例中，该步骤具体所采用的算法如下：

(1)  TimeTransitionRemove(G){(2)  let ET＝{e|e∈G.E ∧e.act＝τ}；(3)  while ET≠ do(4)      choose X from ET(5)      let TT＝{e|e.source＝X.target}；(6)      if TT≠then(7)       for every tt∈TT do(8)         if{X.soruce，tt.action，tt.target}G.E then(9)            G.E:＝G.E∪{X.source，tt.action∈，tt.target}；            fi          od        fi(10)    G.E:＝G.E{X}；      od(11)  while SV＝{v|v∈G.V，e∈G.E，e.target＝v}{G.v₀}≠do(12)    for every vin SV do(13)        G.E:＝G.E{e|e.source＝v}，G.V:＝G.V(v}；          od        od(14)    let i:＝1；(15)    for every e∈G.E do(16)      e.action:＝t_i·e.action，i++；      od(17)  return G；}

其主要思想是将转移图中的抽象时间延迟转移与紧跟其后的动作转移合并，合并的转移只用动作转移来表示，从而将抽象时间延迟转移以及那些只用于表示这种转移的符号状态从转移图中去除。其中，方法第3至10步用于将抽象时间延迟转移从G中去除：方法第11至13步用于删除那些由于去除了显示时间延迟转移而导致在符号状态图中不可达的符号状态及相关转移；方法第14至16步在符号状态图中每一个转移动作之前增加一个用于表示时间迁移的变量ti。

将图5所示的MSTGSS G作为输入，调用上述的算法得到如图6所示的符号状态转移图G’，该图通过将图5中的抽象时间转移以及只用于表示抽象时间转移的符号状态去除之后，只包含6个符号状态，其中每一个转移都是动作转移；另外为了表示动作转移之前的时间延迟量，图6中在每个转移动作前增加了一个时间延迟变量。图6所示的这种转移图称为不含抽象时间转移的稳定符号状态转移图(USTGSS)。USTGSS使用时间变量来统一表示MSTGSS中的抽象时间延迟以及隐含的时间延迟，是对MSTGSS的一种更简洁的表示。

(4)根据不含抽象时间转移的最简稳定符号状态图生成可执行的含时间延迟变量的转移动作序列；

USTGSS中转移标号是由一个时间变量和一个转移动作构成，因为USTGSS具有稳定性，所以生成的转移动作序列一定可行，如果不考虑时间因素，便可以使用时间无关的测试方法来生成转移动作序列。因为USTGSS中不包含确定的时间信息，所以生成的动作序列无法直接执行，故而只能使用静态方法来生成转移动作序列。在转移动作序列的生成过程中，可以考虑各种结构覆盖标准，如状态覆盖、转移覆盖和路径覆盖等等。另外，为了避免生成的动作序列过多，在生成测试用例时还可以引入测试目的，从而只对系统的某一部分或者特定属性进行测试。

(5)执行转移动作序列，并且求解转移动作序列中时间延迟变量的值，生成时间测试用例。

在本实施例中，转移动作序列σ的具体执行过程为：

(1)  RealExecute(G′，σ){(2)  construct a set CON of time constraints according to σ and G′；(3)  let k:＝0，l:＝len(σ)；(4)  while k′sat，k＜k′≤l∧σ[k′]，second∈∑°∧σ[i]，second∈∑ⁱ，k＜i＜k′do(5)    if k′-k＞1 do(6)       calculate every σ[i]，first sat，corresponding constraints in CON，k＜i＜k′；(7)       let i:＝k+1；(8)       while i＜k′do(9)         after time σ[i]，first then execute σ[i]，second；i++；          od      fi(10)  let timer t:＝0，start(t)；(11)  calculate possible value field D of σ[k′]，first according to CON.(12)  while true do(13)     if t Current Value＞Max(D)then return false，fi(14)     if not receive any action then contimte；fi(15)     if receives action α≠σ[k′]，second then return false；(16)     else if t.Current Value＜Min(D)then return false；(17)           else goto(15)；fi         fi       od(18)   let t_k′＝t.Current Value，k:＝k′    od(19)return true；}

其中，第2步首先根据符号状态转移系统G和转移动作序列σ建立一个线性约束系统CON；因为系统输出动作的时间无法控制，因而第4-6步利用线性约束求解方法求解时间变量时，只对到下一个输出动作之前所有输入动作前的时间延迟量进行求解；第7-9步根据所求得的时间延迟量来执行相应的输入动作；第10-17步处理被测系统期望的输出动作，如果输出动作不是所期望的或者等待时间不满足约束限制，则返回false，否则继续执行。

因为测试系统对被测系统只具有有限的观察性，如果一个输入动作之后没有输出动作，那么便无法判断该输入动作是否被正确地执行，故而上述执行过程中只执行σ中最后一个输出动作便返回。

其中，第6步在采用线性约束求解方法求解时间延迟变量值时，满足时间约束的时间延迟变量的解往往是一个实数集合，因此必须考虑如何从中选择适合的解来执行测试。这里我们的策略是选择时间延迟变量的极值来执行测试，以便能够更加有效地检测系统中存在的错误。为了能够选择时问延迟变量的极值来执行转移动作序列，我们在方法中引入极值函数fun。考虑到线性约束求解方法的能力，fun可以是上述执行过程中第6步中所涉及的时间变量构成的线性函数。在上述执行过程的第6步求解时间延迟变量时，除了要满足系统中相应的时间约束条件，还必须让函数fun取极大或极小值。实际的测试执行过程中，用户可以根据不同的测试目的来选择相应的极值函数。例如，为了测试一个转移动作序列的最长(短)时间执行过程，可以将极值函数定义为所涉及的所有时间变量之和。

(6)报告测试执行结果。

实施例二：基于时间输入输出自动机模型的测试系统

根据上述实施例一中所描述的方法，用于实现该方法的一个软件系统的组成如图2所示，该系统包括：系统建模器，用于实现实施例一中的步骤(1)；模型转换器，其包括时间自动机化简模块和时间转移去除模块，分别用于实现步骤(2)和(3)；转移动作生成器，用于实现步骤(4)，测试用例生成和执行器，用于实现步骤(5)，其包括线性约束求解模块、测试用例生成模块和测试用例执行模块；测试执行接口，用于实现所述测试用例生成和执行器与测试管理器之间的连接，测试用例中所有的输入转移动作均通过测试执行接口发送给被测系统，同时，测试系统也通过测试执行接口来接收所有被测系统的输出转移动作。

以上对本发明所述的基于时间安全输入输出自动机的测试方法及其进行了详细的说明，但显然本发明的具体实现形式并不局限于此。对于本技术领域的一般技术人员来说，在不背离本发明所述方法的精神和权利要求范围的情况下对它进行的各种显而易见的改变都在本发明的保护范围之内。