• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>10th International Workshop on Abstract State Machines 2003: Advances in Theory and Practice ASM 2003, Mar 3-7, 2003, Taormina, Italy >Using Spin to Generate Tests from ASM Specifications
【24h】

Using Spin to Generate Tests from ASM Specifications

机译：使用Spin从ASM规范生成测试

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In this paper we introduce an algorithm to automatically encode an ASM specification in PROMELA, the language of the model checker Spin, and we present a method exploiting the counter example generation feature of Spin, to automatically generate from ASM specifications test sequences which accomplish a desired coverage. ASMs are used as test oracles to predict the expected outputs of units under test. A prototype tool that implements the proposed method is also presented. Experimental results in evaluating the method are reported. The experiments include test sequence generation, tests execution, code coverage measurement for a case study implemented in Java, and comparison with random tests generation. Benefits and limitations in using model checking are discussed.
机译：在本文中，我们介绍了一种在PROMELA（模型检查器Spin的语言）中自动对ASM规范进行编码的算法，并提出了一种利用Spin的反例生成功能从ASM规范自动生成完成所需目标的测试序列的方法覆盖范围。 ASM用作测试预言机，以预测被测设备的预期输出。还介绍了实现所提出方法的原型工具。报告了评估该方法的实验结果。实验包括测试序列生成，测试执行，针对以Java实现的案例研究的代码覆盖率度量，以及与随机测试生成的比较。讨论了使用模型检查的好处和局限性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号