• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >An Iterative Framework for Simulation Conformance
【24h】

An Iterative Framework for Simulation Conformance

机译：仿真一致性的迭代框架

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

摘要

MAGIC is a software verification project for C source code which verifies conformance of software components against state-machine specifications. To this aim, MAGIC extracts abstract software models using predicate abstraction, and resolves the inherent trade-off between model accuracy and scalability by an iterative abstraction refinement methodology. This paper presents the core principles implemented in the MAGIC verification engine, i.e. specification conformance using simulation and abstraction refinement. Viewing counterexamples as winning strategies in a simulation game between the implementation and the specification, we describe an algorithm where abstractions are refined on the basis of multiple winning strategies simultaneously. The refinement process is iterated until either a conformance with the specification is established, or a strategy to violate the specification is found to be realizable. In addition to the increase in expressiveness achieved by using simulation instead of trace containment, experimental results using OpenSSL indicate that our approach can lead to orders of magnitude improvement in verification time.
机译：MAGIC是用于C源代码的软件验证项目，该项目可验证软件组件是否符合状态机规范。为此，MAGIC使用谓词抽象提取抽象软件模型，并通过迭代抽象细化方法解决了模型准确性和可伸缩性之间的固有权衡。本文介绍了MAGIC验证引擎中实现的核心原理，即使用仿真和抽象提炼的规范一致性。通过在实现和规范之间的模拟游戏中查看反例作为获胜策略，我们描述了一种算法，其中基于多个获胜策略同时完善抽象。反复进行优化过程，直到建立与规范的一致性，或者发现可以实现违反规范的策略为止。除了通过使用模拟而不是跟踪约束来提高表达能力之外，使用OpenSSL进行的实验结果还表明，我们的方法可以导致验证时间缩短多个数量级。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号