• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE Pacific Rim International Symposium on Dependable Computing >Method and Case Study of Model Checking Concurrent Systems That Use Unbounded Timestamps
【24h】

Method and Case Study of Model Checking Concurrent Systems That Use Unbounded Timestamps

机译：使用无限制时间戳的并发系统模型检查的方法和案例研究

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Parallel and distributed algorithms, including those for fault tolerance, often use timestamps to coordinate the behaviors of processes. These algorithms are hard to correctly design and often subject to subtle design faults. Model checking, which is a state exploration-based verification method, has been very successful in finding design faults in many practical systems. However model checking of timestamp-based algorithms is difficult when the values of timestamps are not bounded, because then the state space is infinite. This paper addresses the problem of infinite state space by proposing a data abstraction technique for timestamps. This technique transforms the infinitestate algorithm to a finite-state abstract model which simulates the original algorithm. The applicability of this approach is demonstrated through a case study where Lamport's bakery algorithm is verified in the absence and presence of process failures.
机译：并行和分布式算法（包括用于容错的算法）通常使用时间戳来协调流程的行为。这些算法难以正确设计，并且经常会遭受细微的设计错误。模型检查是一种基于状态探索的验证方法，已成功地发现了许多实际系统中的设计错误。但是，当时间戳的值不受限制时，基于时间戳的算法的模型检查将很困难，因为状态空间是无限的。本文通过提出一种用于时间戳的数据抽象技术来解决无限状态空间的问题。该技术将无限状态算法转换为模拟原始算法的有限状态抽象模型。通过案例研究证明了该方法的适用性，在该案例研究中，在不存在和存在过程故障的情况下，验证了兰莫特的烘焙算法。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号