不可靠环境下多轮FR协议分析

Failure Analysis of Multiple Runs of FR Protocol Using Model Checking

随着网络的大规模应用,越来越多的协议在并发的、不可靠的环境中执行。文章用有限自动机对FR协议建模,并用自动验证工具UPPAAL验证了多轮协议在可靠环境下的性质。重点验证了不可靠环境中多轮协议的执行情况,最后对协议进行了修改。

With the growing popularity of the lnternet,more and more protocols run concurrently.In this paper,finite state automata is used to model FR protocol.Then UPPAAL is used to verify some properties of the protocol when the site or communication is reliable.Thls paper focuses on multiple runs of FR protocol in the presence of site or comunication failure.