摘  要： 实时系统是指与运行环境的交互行为存在时间约束的系统。由于时间约束的无穷状态空间问题，增加了实时系统测试难度。本文基于时间自动机，利用时间区域分解的方法，将无穷状态空间的时钟区域在时钟数量对应的坐标图中等价划分为各个类，在生成的测试路径中取到相应的点坐标，简化取点的个数，有效减少测试用例的生成数量，进而相对减少状态空间爆炸的可能性，为实时系统功能、安全性验证提供理论基础。

　　关键词： 实时系统；区域分解；时间自动机；状态空间；测试用例

0 引言

　　随着计算机系统在航空航天、轨道交通、工业控制和核反应控制等安全苛求系统中的广泛应用，如何有效地保障这类系统的安全性与可靠性成为行业着重解决的关键问题。而实时性是影响这类系统安全性的关键特性，如何检测和验证该类系统满足实时性能需求成为保证系统安全的关键技术。而实时系统因增加时间约束，加速了这类系统状态空间爆炸，而无法保证这类系统的完备测试和验证。常见的该类系统的测试方法主要包括静态时间分析和动态实时测试。静态分析方法通过预估计程序执行的时间判定时间约束的满足性；动态测试是在系统仿真执行时调用时钟部件进行任务执行时间测算，从而判定时间约束的满足性。但这类测试方法难以应用到基于模型驱动的实时测试问题中。

　　时间维覆盖满足性问题成为基于模型驱动的实时测试的关键问题，常见的基于模型的测试方法多采用随机选取时间满足点替代时间区间的测试，或采用状态空间与后继迁移的空间交集分解后再选取随机点的方法，这类方法都无法满足时间点覆盖需求。本文提出一种基于时间自动机模型的测试用例生成方法，将时钟区域等价划分，使得每个区域的时钟值表示相同行为[1]，生成数量少、覆盖点完备的测试用例集合。

1 时间自动机[2-4]及其状态空间

　　对于时钟集合C，时钟约束[3，5]集合Ф（C）={Ф|Ф是一个时钟约束}，其中Ф是时间自动机的基本组成成分，是实时系统模型检查算法操作的基础，定义：Ф=x∞n|x-y∞n∞，x、y∈C，n∈N。

　　一个时间自动机T可以表示为一个多元组（L，l0，C，A，E，I）[1，2，6]，其中：

　　（1）L是一个有限状态的集合；

　　（2）l0是初始状态，是L的子集；

　　（3）C是一个有限的时钟集合，所有的时钟在l0处初始化为零；

　　（4）A是一个有限的标记集合；

　　（5）E是一个映射，给每一个位置L指定Ф（C）中的某个时钟约束；

　　（6）I是一个状态迁移的集合，其中E?哿L×A×2C×Ф（C）×L。一个迁移（s，a，u，λ，s′）表示当输入符号a时从状态s转移到状态s′，u是X上的一个时钟约束条件，即u∈Ф（C），它指定迁移的发生时间，集合λ∈X给出在状态转移发生时被重置的时钟。

　　时间自动机T的语义由一个与它相关的系统S定义，其状态扩展为<s，v>，其中s为A的某一状态，v是一个时钟解释。如果s是A的初始位置，并且对于所有的时钟变量x都有v（x）=0，那么状态（v，s）便是一个初始状态。在迁移系统中有如下两种类型的迁移[5，7]：

　　（1）时间流逝迁移：对一个状态（s，v）和一个实数的时间增量d≥0，如果对所有的d≥d′≥0，v+d′∈l（s），则（s，v）（s，v+d）；

　　（2）动作迁移：对于一个状态（s，v）和一个迁移（s，a，u，λ，s′），其中v∈u，则（s，v）（s′，v′）。

2 时间状态空间的计算及测试用例生成技术

　　2.1 时间状态空间的计算

　　划分时钟区域要求时间的整数部分一致，并且所有时钟间的小数部分的变化顺序也一致。整数部分决定是否满足指定的时钟约束，而小数部分的先后顺序决定哪个时钟会先改变其整数部分。为了更好地说明，将区域划分为三种类别[1]：拐点区域、开线段区域和开区域。时钟区域的计算要同时考虑时钟的个数以及一个迁移是输入还是输出。CR表示时钟区域的数目，C表示时钟的个数，Cx、Cy表示时间约束的长度。

　　当时钟数为1，即C=1时，如图1，给出了此时的区域最小数的情况，区域数为4，即2个拐点区域+2个开线段区域。而当Cx增加最小量1时，拐点区域和开线段区域都相应地增加1，也就是说，Cx每增加1，区域总数CR相应增加2。由此可以得到，当只有一个时钟即C=1时，区域总数CR=4+（2×（Cx-1））=2×（Cy+1）。

　　当时钟数为2，即C=2时，时钟值用相应的二维坐标来表示，每个坐标轴代表一个时钟，如图2给出了当Cx=Cy=1时的最小区域数。从图中可以看出此时的区域个数为18，可以推算出当时钟数C=2时，区域总数CR=（6×Cx×Cy）+4×（Cx+Cy+1）。

　　当时钟数为3，即C=3时，时钟值用相应的三维坐标来表示，同样可以推算出此时的区域总数CR=（22×Cx×Cy×Cz）+10×（Cx×Cy+Cx×Cz+Cy×Cz）+8×（Cx+Cy+Cz+1）[1]。

　　划分的区域可以简化取点的个数，进而减少生成的测试用例的数量。例如若在图2中取点（0.65，0.5）和（0.72，0.6），根据上述的等价划分方法，在这里可认为二者是等价的，即二者对应生成的路径是一样的。

　　2.2 测试用例生成技术

　　（1）首先根据所给自动机模型的实例，分析系统中全部可能的状态。如一个有穷状态机[8]M（X，Y，Q，q0，ε，O），其中X={a，b}是一个输入符号集合，Y={0，1}是一个输出符号集合，Q={q0，q1，q2}是一个有穷的状态集合，q0是初始状态，ε是状态转换函数，O是输出函数。对M来说，系统中的全部可能的状态即为q0，q1，q2[8]。然后将全部的状态空间按时间维展开为时间状态空间。即将模型中的各个状态位置分别和一个时间域一起构成符号状态以生成有限状态模型，也就是对位置赋一个时间不变量。迁移动作发生时的时钟值需要满足一定的约束条件，才能发生状态的迁移。

　　（2）由时间状态空间生成相应的路径。当满足发生迁移的时间约束和迁移约束时，迁移发生，从一个状态迁移到另一个状态，最终形成路径。

　　（3）任取路径按相应时间维数的区域计算方法，生成路径上每个点的时间区域类，并按2.1节中介绍到的区域点选取规则，产生该点的区域样点。

　　（4）根据每条路径的约束规则，选取路径点的时间样点的组合点，形成该条路径的满足时间维的测试用例。

3 案例分析

　　对单一路径来说，系统中每条路径中的边和时间的取点不尽相同。根据时钟数量的不同，每个时钟对应的约束不同，其相应的取点也就不同，举一个简单的列车通过道口的例子，如图3。状态A（approach）表示列车接近道口，O（open）表示道口打开，C（close）表示道口关闭，即状态Q={A，O，C}有三个。当满足时间约束t<3时，状态由A迁移到O，此时时间重置为0。当列车接近满足t<5时，道口打开，此时再判断t的大小，若是t>3，则列车等待（wait），状态由O回到A，重新判断；若是t<3，状态由O迁移到C，则列车通过（cross），此时t重置为0。若t<2则道口关闭（close），状态C到达起点A，同时，时间t重新置为0。

　　对应上例，根据2.1节介绍的区域点选取规则，可能会生成如下的测试用例：

　　（0）.open→（0）.cross→（1）.close

　　（0）.open→（0.5）.cross→（1）.close

　　（0）.open→（1）.cross→（1）.close

　　（0）.open→（1.5）.cross→（1）.close

　　（0）.open→（2）.cross→（1）.close

　　（0）.open→（2.5）.cross→（1）.close

　　（0）.open→（3）.cross→（1）.close

　　（0）.open→（3.5）.wait

　　（0）.open→（4）.wait

4 总结

　　本文利用时间自动机模型来描述实时系统，分析系统状态空间，提出面向时间维模式的状态空间计算方法，将区域划分为不同类别，简化了时钟区域的取值。然后介绍了计算时钟区域数量的方法。最后给出具体的生成测试用例的实例。后期研究内容包括对时钟区域的进一步划分，进而减少生成测试用例的数量。

参考文献

　　[1] ABOUTRAB M S. Testing real-time embedded systems using timed automata based approaches[J]. The Journal of Systems and Software 2013（86）：1209-1216.

　　[2] ALUR R， DILL D L. A theory of timed automata[J]. Theoretical Computer Science，1994，126（2）：183-235.

　　[3] ALUR R. Timed automata[J]. Computer Aided Verification. Springer Berlin Heidelberg， 1999：8-22.

　　[4] ALUR R， COURCOUBETIS C， DILL D. Model-checking for real-time systems[C]. Logic in Computer Science， 1990， LICS′90， Proceedings， Fifth Annual IEEE Symposium on e. IEEE， 1990：414-425.

　　[5] 孙全勇.时间自动机及其应用研究[D].哈尔滨：哈尔滨工程大学，2007.

　　[6] ABOUTRAB M S， COUNSELL S， HIEROINS R M. GeTeX： a tool for testing real-time embedded systems using CAN applications[C]. 18th IEEE International Conference and Workshops on Engineering of Computer-Based Systems，2011：61-70.

　　[7] 陈伟，薛云志，赵琛，等.一种基于时间自动机的实时系统测试方法[J].软件学报，2007，18（1）：62-73.

　　[8] MATHUR A P.软件测试基础教程[M].王峰，郭长国，陈振华，等，译.北京：机械工业出版社，2011.