• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>IEEE Transactions on Parallel and Distributed Systems >Computer aided verification of Lamport's fast mutual exclusion algorithm using colored Petri nets and occurrence graphs with symmetries
【24h】

Computer aided verification of Lamport's fast mutual exclusion algorithm using colored Petri nets and occurrence graphs with symmetries

机译：兰佩特快速互斥算法的计算机辅助验证，使用有色Petri网和具有对称性的出现图

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

摘要

In this paper, we present a computer tool for verification of distributed systems. As an example, we establish the correctness of Lamport's Fast Mutual Exclusion Algorithm. The tool implements the method of occurrence graphs with symmetries (OS-graphs) for Colored Petri Nets (CP-nets). The basic idea in the approach is to exploit the symmetries inherent in many distributed systems to construct a condensed state space. We demonstrate a significant increase in the number of states which can be analyzed. The paper is to a large extent self-contained and does not assume any prior knowledge of CP-nets (or any other kinds of Petri Nets) or OS-graphs. CP-nets and OS-graphs are not our invention. Our contribution is the development of the tool and verification of the example, demonstrating how the method of occurrence graphs with symmetries can be put into practice.
机译：在本文中，我们提出了一种用于验证分布式系统的计算机工具。例如，我们确定了兰莫特的快速互斥算法的正确性。该工具为彩色Petri网（CP-net）实现了具有对称性的出现图方法（OS-图）。该方法的基本思想是利用许多分布式系统中固有的对称性来构造一个压缩状态空间。我们证明可以分析的状态数量显着增加。本文在很大程度上是独立的，并且不假定您具有CP网络（或任何其他种类的Petri网络）或OS图形的任何先验知识。 CP网络和OS图形不是我们的发明。我们的贡献是开发了工具并验证了示例，演示了如何将具有对称性的发生图方法应用于实践。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号