将SMT求解器应用于测试模板框架
软件工程
2012-02-29 v1
摘要
测试模板框架（TTF）是一种针对Z符号的基于模型的测试方法。在TTF中，测试用例从测试规约（用Z编写的谓词）生成。而Z符号基于带等式的一阶逻辑和Zermelo-Fraenkel集合论。因此，测试用例是满足该理论中公式的一个见证。可满足性模理论（SMT）求解器是软件工具，用于判定大量内置逻辑理论及其组合中任意公式的可满足性。在本文中，我们展示了应用两个SMT求解器Yices和CVC3作为引擎从TTF的测试规约中寻找测试用例的初步结果。为此，我们提供了Z符号重要部分的浅嵌入到Yices和CVC3的输入语言中，因为它们不直接支持Z中定义的Zermelo-Fraenkel集合论。最后，分析了将这些嵌入应用于八个案例研究的多个测试规约的结果。
引用
@article{arxiv.1202.6120,
title = {Applying SMT Solvers to the Test Template Framework},
author = {Maximiliano Cristiá and Claudia Frydman},
journal= {arXiv preprint arXiv:1202.6120},
year = {2012}
}
备注
In Proceedings MBT 2012, arXiv:1202.5826