...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>International journal of parallel programming >Verification Approach of Metropolis Design Framework for Embedded Systems
【24h】

Verification Approach of Metropolis Design Framework for Embedded Systems

机译：嵌入式系统Metropolis设计框架的验证方法

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

摘要

In this paper, we focus on the verification approach of Metropolis, an integrated design framework for heterogeneous embedded systems. The verification approach is based cm the formal properties specified in Linear Temporal Logic (LTL) or Logic of Constraints (LOC). Designs may be refined due to synthesis or be abstracted for verification. An automatic abstraction propagation algorithm is used to simplify the design for specific properties. A user-defined starting point may also be used with automatic propagation. Two main verification techniques are implemented in Metropolis: the formal verification utilizing the model checker Spin and the simulation trace checking with automatic generated checkers. Translation algorithms from specification models to verification models, as well as algorithms of generated checkers are discussed. We use several case studies to demonstrate our approach for verification of system level designs at multiple levels of abstraction.
机译：在本文中，我们关注于Metropolis的验证方法，Metropolis是一种用于异构嵌入式系统的集成设计框架。验证方法基于线性时间逻辑（LTL）或约束逻辑（LOC）中指定的形式属性。设计可以由于综合而完善，也可以抽象化以用于验证。自动抽象传播算法用于简化特定属性的设计。用户定义的起点也可以与自动传播一起使用。在Metropolis中实现了两种主要的验证技术：使用模型检查器Spin的形式验证和使用自动生成的检查器进行的模拟跟踪检查。讨论了从规范模型到验证模型的转换算法，以及生成的检查器算法。我们使用一些案例研究来展示我们在多个抽象级别上验证系统级别设计的方法。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号