• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>12th International Conference on CONCUR 2001 - Concurrency Theory, 12th, Aug 20-25, 2001, Aalborg, Denmark >Channel Representations in Protocol Verification
【24h】

Channel Representations in Protocol Verification

机译：协议验证中的通道表示

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

摘要

In automated verification of protocols, one source of complications is that channels may have unbounded capacity, in which case a naive model of the protocol is no longer finite state. Symbolic techniques have therefore been developed for representing the contents of unbounded channels. In this paper, we survey some of these techniques and apply them to a simple leader election protocol. We consider protocols with entities modeled as finite state machines which communicate by sending messages from a finite alphabet over unbounded channels; this is a framework for which many techniques have been developed. We also consider a more general model in which messages may belong to an unbounded domain of values which may be compared according to a total ordering relation: the motivation is to study protocols with timestamps or priorities. We show how techniques from the previous setting can be extended to this more general model, but also show that reachability quickly becomes undecidable if channels preserve the ordering between messages.
机译：在协议的自动验证中，复杂性的一个来源是通道可能具有无限制的容量，在这种情况下，协议的简单模型不再是有限状态。因此，已经开发出用于表示无边界信道的内容的符号技术。在本文中，我们调查了其中一些技巧，并将其应用于简单的领导者选举协议。我们考虑将实体建模为有限状态机的协议，这些实体通过在有限通道上通过有限字母发送消息来进行通信；这是已经开发出许多技术的框架。我们还考虑了一个更通用的模型，其中消息可能属于值的无限制域，可以根据总排序关系对其进行比较：动机是研究带有时间戳或优先级的协议。我们展示了如何将先前设置中的技术扩展到这个更通用的模型，而且还展示了如果通道保留消息之间的顺序，则可到达性很快变得不确定。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号