Generation of test sequences from formal specifications: GSM 11‐11 standard case study
Generation of test sequences from formal specifications: GSM 11‐11 standard case study
复制标题
根据正式规范生成测试序列：GSM 11‐11 标准案例研究
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
F. Peureux
中科院分区：
文献类型：
--
作者：
Eddy Bernard;B. Legeard;Xavier Luck;F. Peureux
本文介绍了为智能卡GSM 11‐11标准的一个片段生成测试用例的案例研究结果。生成方法是基于一种原始的方法，使用B符号和集合约束逻辑规划技术。GSM 11‐11技术规范以B符号形式化。从这个B规范中，导出了一个约束系统，等价于这个形式模型。利用集合约束求解器，通过遍历规范的约束可达性图，计算边界状态，得到测试用例。该项目的目的是通过将生成的测试序列与已经使用的高质量手动设计的测试进行比较，评估这种称为B - testing - TOOLS的测试环境在实际应用中的工业过程中的贡献。这种比较使我们能够验证我们的方法，并显示其在关键应用程序验证过程中的有效性：与预先存在的测试相比，案例研究提供了广泛的生成测试覆盖率（约85%），并节省了30%的测试设计时间。版权所有©2004 John Wiley & Sons， Ltd
This paper presents the results of a case study on generating test cases for a fragment of the smart card GSM 11‐11 standard. The generation method is based on an original approach using the B notation and techniques of constraint logic programming with sets. The GSM 11‐11 technical specifications were formalized with the B notation. From this B specification, a system of constraints was derived, equivalent to this formal model. Using a set constraint solver, boundary states were computed and test cases were obtained by traversing the constrained reachability graph of the specifications. The purpose of this project was to evaluate the contribution of this testing environment, called B‐TESTING‐TOOLS, in an industrial process on a real life‐size application, by comparing the generated test sequences with the already used and high‐quality manually‐designed tests. This comparison enabled us to validate our approach and showed its effectiveness in the validation process of critical applications: the case study gives a wide coverage (about 85%) of the generated tests compared to the pre‐existing tests and a saving of 30% in test design time. Copyright © 2004 John Wiley & Sons, Ltd.