一种基于时间自动机的实时系统测试方法

基于时间自动机(timedautomata,简称TA)的一种变体——时间安全输入/输出自动机(timedsafetyinput/outputautomata,简称TSIOA),提出了一种实时系统测试方法.该方法首先将时间安全输入/输出自动机描述的系统模型转换为不含抽象时间延迟迁移的稳定符号状态迁移图(untimedstabletransitiongraphofsymbolicstate,简称USTGSS);然后采用基于标号迁移系统(labeledtransitionsystem,简称LTS)的测试方法来静态生成满足各种结构覆盖标准的包含时间延迟变量迁移动作序列;最后,给出了一个根据迁移动作序列构造和执行测试用例的过程,该过程引入了时间延迟变量目标函数,并采用线性约束求解方法动态求解迁移动作序列中的时间延迟变量.

一种符号化执行的实时系统一致性测试生成方法

系统一致性测试用来验证和确认系统实现的正确性.针对实时系统在进行数据处理时受到时间约束,容易导致状态空间爆炸的问题,提出一种符号化测试生成方法.首先对符号变迁系统和时间自动机进行扩展,建立一种新的符号语义模型TSIOSTS,基于该模型定义了时间一致性关系(tioco);然后以tioco关系为指导,结合符号化执行策略,生成被测系统模型的时间符号化测试行为树,并转化为测试用例;最后将提出的理论和方法应用于CTCS-3列控系统临时限速服务器的一致性测试中,验证了该方法的可行性和有效性.

基于符号执行和LTL公式重写的测试用例产生方法

基于模型检验等形式化方法的测试用例自动产生技术成为测试自动化领域一项重要的进展.对于输入和输出为无界抽象数据类型的无限状态系统,利用传统模型检验技术难以有效地产生测试用例集合,提出基于符号执行和公式重写的测试用例产生方法.通过建立程序的符号化执行模型,避免输入和输出变量数值化枚举而导致的无限状态系统的建模和状态爆炸问题;建立基于符号化执行模型的时序公式重写规则,并根据线性时序逻辑(linear temporal logic,LTL)公式的反例模式求取复杂属性及行为约束关系,利用约束求解的方法自动产生测试用例集合.这种方法集成了符号执行技术和时序公式状态重写——一种轻量级模型检验技术,成为基于复杂抽象数据类型系统与属性相关的测试用例自动产生的有效方法.

网络协议测试的符号化一致性关系研究

协议的一致性测试可以验证协议实现的正确性,一致性关系是测试生成的基础。网络协议的特点之一是控制消息中会携带大量数据。针对网络协议的该特点提出了符号化的一致性关系模型。建立了网络协议的输入输出符号变迁系统,并且依据数据符号实例化策略建立了对应的语义模型,在该模型中系统的活动是集成控制和数据的复杂活动。在此输入输出符号变迁模型的基础上提出了一种符号化的一致性关系以生成测试套。为了便于测试套的自动生成,对所提出的一致性关系进行了简化。在上述过程中数据的处理通过符号化的变量进行建模,这样可以使用统一符号进行数据处理,而不必总是关心具体的数值,只需在适当的时机进行符号的实例化。文中所提出的一致性关系模型充分利用了符号化的变量,增加了该模型的抽象程度,避免了处理过程的复杂性,且可以指导测试套的自动生成。最后使用IPv6的邻居发现协议对该一致性关系进行了说明。