...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>IEEE Transactions on Software Engineering >Integrating formal verification and conformance testing for reactive systems
【24h】

Integrating formal verification and conformance testing for reactive systems

机译：集成反应系统的形式验证和一致性测试

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

摘要

In this paper, we describe a methodology integrating verification and conformance testing. A specification of a system - an extended input-output automaton, which may be infinite-state - and a set of safety properties ("nothing bad ever happens") and possibility properties ("something good may happen") are assumed. The properties are first tentatively verified on the specification using automatic techniques based on approximated state-space exploration, which are sound, but, as a price to pay for automation, are not complete for the given class of properties. Because of this incompleteness and of state-space explosion, the verification may not succeed in proving or disproving the properties. However, even if verification did not succeed, the testing phase can proceed and provide useful information about the implementation. Test cases are automatically and symbolically generated from the specification and the properties and are executed on a black-box implementation of the system. The test execution may detect violations of conformance between implementation and specification; in addition, it may detect violation/satisfaction of the properties by the implementation and by the specification. In this sense, testing completes verification. The approach is illustrated on simple examples and on a bounded retransmission protocol.
机译：在本文中，我们描述了一种整合验证和一致性测试的方法。假定系统是规范的-可能是无限状态的扩展输入输出自动机-并具有一组安全属性（“什么都不会发生”）和可能性属性（“可能会发生”）。首先使用基于近似状态空间探索的自动技术在规范上临时验证属性，这是合理的，但是作为给自动化付出的代价，对于给定的属性类别，这些属性并不完整。由于这种不完整和状态空间爆炸，验证可能无法成功证明或证明特性。但是，即使验证没有成功，测试阶段也可以继续进行，并提供有关实施的有用信息。测试用例是从规范和属性中自动生成的，并在系统的黑盒实现中执行。测试执行可以检测到实现与规范之间不一致的情况。另外，它可以通过实现方式和规范来检测对属性的违反/满意。从这个意义上说，测试完成了验证。在简单示例和有界重传协议上说明了该方法。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号