• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Programming languages and systems >Towards a Certified Petri Net Model-Checker
【24h】

Towards a Certified Petri Net Model-Checker

机译：获得认证的Petri Net模型检查器

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

摘要

Petri nets are widely used in the domain of automated verification through model-checking. In this approach, a Petri Net model of the system of interest is produced and its reachable states are computed, searching for erroneous executions. Model compilation can accelerate this analysis by generating code to explore the reachable states. This avoids the use of a fixed exploration tool involving an "interpretation" of the Petri net structure. In this paper, we show how to compile Petri nets targeting the LLVM language (a high-level assembly language) and formally prove the correctness of the produced code. To this aim, we define a structural operational semantics for the fragment of LLVM we use.
机译：Petri网广泛用于通过模型检查进行自动验证的领域。用这种方法，生成了感兴趣系统的Petri Net模型，并计算了其可达状态，以寻找错误的执行。模型编译可以通过生成代码来探索可到达的状态来加速这种分析。这避免了使用固定的探索工具，该工具涉及对陪替氏网络结构的“解释”。在本文中，我们展示了如何针对LLVM语言（一种高级汇编语言）编译Petri网，并正式证明了所生成代码的正确性。为此，我们为所使用的LLVM片段定义了结构化的操作语义。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号