• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer aided verification >Distributed Explicit State Model Checking of Deadlock Freedom
【24h】

Distributed Explicit State Model Checking of Deadlock Freedom

机译：死锁自由的分布式显式状态模型检查

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

摘要

This paper presents a practical method and associated tool for verifying deadlock freedom properties in guarded command systems. Such properties are expressed in CTL as AGEF q where q is a set of quiescent states. We require the user to provide transitions of the system that are "helpful" in reaching quiescent states. The distributed search constructs a path consisting of helpful transitions from each reachable state to a state that is either quiescent or is known to have a path to a quiescent state. We extended the PReach model-checker with these algorithms. Performance measurements on both academic and industrial large-scale models shows that the overhead of checking deadlock-freedom compared with state-space enumeration alone is small.
机译：本文提出了一种在受保护的命令系统中验证死锁自由属性的实用方法和相关工具。这样的特性在CTL中表示为AGEF q，其中q是一组静态。我们要求用户提供对达到静止状态“有帮助”的系统转换。分布式搜索构建了一条路径，该路径包括从每个可达状态到静态或已知具有到静态状态的路径的有用转换。我们使用这些算法扩展了PReach模型检查器。在学术和工业大规模模型上的性能测量表明，与仅使用状态空间枚举相比，检查死锁自由的开销很小。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号