• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Software engineering and formal methods >Combining Abstract Interpretation with Symbolic Execution for a Static Value Range Analysis of Block Diagrams
【24h】

Combining Abstract Interpretation with Symbolic Execution for a Static Value Range Analysis of Block Diagrams

机译：结合抽象解释和符号执行，进行框图的静态值范围分析

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

摘要

This paper presents a fully automatic verification technique for Simulink block diagrams, by combining a static value range analysis with symbolic execution. Our concept avoids a translation to other languages and, instead, extracts all necessary attributes from Simulink and interprets the model directly. With this technique, we show how user defined specifications can be validated using sound abstractions for primitives, including IEEE-754 floats, and custom data types. Moreover, we propose optimizations by exploiting the benefits of intervals and symbolic representations to apply our technique to larger models. We evaluate our solution against an industrial tool.
机译：本文通过将静态值范围分析与符号执行相结合，提出了一种针对Simulink框图的全自动验证技术。我们的概念避免了翻译成其他语言，而是从Simulink中提取了所有必要的属性并直接解释了模型。使用这种技术，我们展示了如何使用原始的声音抽象（包括IEEE-754浮点数和自定义数据类型）来验证用户定义的规范。此外，我们通过利用间隔和符号表示的优势提出优化建议，以将我们的技术应用于更大的模型。我们根据工业工具评估我们的解决方案。

著录项

  • 来源
  • 会议地点 Vienna(AU)
  • 作者

    Christian Dernehl; Norman Hansen; Stefan Kowalewski;

  • 作者单位

    RWTH Aachen University, Lehrstuhl Informatik 11 - Embedded Software, Aachen, Germany;

    RWTH Aachen University, Lehrstuhl Informatik 11 - Embedded Software, Aachen, Germany;

    RWTH Aachen University, Lehrstuhl Informatik 11 - Embedded Software, Aachen, Germany;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号