孙　晶　金晓文

(北方工业大学信息工程学院　北京 100144)



模型检测引导的TTCN-3测试套生成技术研究

孙晶金晓文

(北方工业大学信息工程学院北京 100144)

针对软件测试的不完备性以及软件测试自动化问题，提出在测试过程中将模型检测前置于传统测试，将模型检测与测试相结合。通过分析模型检测中的形式化规约明确测试目的，并转换成TTCN-3(Testing and Test Control Notation) 抽象测试套。进一步利用规约中本身存在的正例，与数据类型描述文件相关联，从而生成测试用例。分析TTCN-3开发模式，基于标签转换系统与TTCN-3行为树的等价性，提出模型检测引导的抽象测试套生成算法，并实现TTCN-3抽象测试套的自动生成。

软件测试模型检测TTCN-3测试套μ演算

0　引　言

近年来，模型检测以其自动化程度高的特点在软件测试领域得到了广泛关注。由于模型检测可以自动执行，并能在系统不满足性质时提供反例路径来说明不满足的原因，因此在工业界比演绎证明更受推崇。而测试是保证软件产品可靠性和正确性的传统手段，相较模型检测而言自动化不高，手动选取测试用例有不完备性。

模型检测是关于自动验证并行或者分布式系统性质的算法和方法，它的基本思想是用状态迁移系统(S)表示系统的行为，用模态逻辑公式(F)描述系统的性质。这样“系统是否具有所期望的性质”就转化为数学问题“状态迁移系统S是否是公式F的一个模型？”，用公式表示为S╞F[1]。对有穷状态系统，这个问题是可判定的，即可以用计算机程序在有限时间内自动确定。……