在存在节点故障时使用PALS架构验证无线多跳网络的分布式拓扑控制协议
计算机科学中的逻辑
2010-09-24 v1
摘要
PALS架构在合理的要求下，将分布式实时异步系统的设计简化为同步系统的设计。假设逻辑同步性减少了系统行为，并为工程目的提供了概念上更简单的范式。该框架目前的局限性之一是，必须从一组独立的“同步机器”中手工组合出整个同步系统，这既繁琐又容易出错。我们使用Maude的元层，根据用户提供的组件机器以及机器间如何相互通信的描述，自动生成同步组合。然后，我们利用这一新功能验证了在可能发生故障的节点存在时，无线网络分布式拓扑控制协议的正确性。
引用
@article{arxiv.1009.4601,
title = {Using the PALS Architecture to Verify a Distributed Topology Control Protocol for Wireless Multi-Hop Networks in the Presence of Node Failures},
author = {Michael Katelman and José Meseguer},
journal= {arXiv preprint arXiv:1009.4601},
year = {2010}
}
备注
In Proceedings RTRTS 2010, arXiv:1009.3982