通信协议的自稳定性及其验证方法

Self stabilization and Its Verification Methods of Communication Protocols

提出了通信协议自稳定性的两种验证方法．以ＴＣＰ／ＩＰ网络的滑动窗口协议为例，给出它的基于谓词逻辑形式描述的两个文本，前者只是安全的，后者是安全的且是自稳定的．并由此说明自稳定通信协议能使协议中的进程重建彼此之间的协同，从而大大提高协议的可靠性．

Two verification mothods for self stabilization of communication protocols are put forward. As an example of sliding window protocol in TCP/IP network, two formal specification texts are given based on predicate logic. The former is safe. The latter is not only safe but self stabilization. It is proved that stabilizing communication protocol obliges the processes in the protocol to re establish coordination amony them, and greatly improves reliability of the protocal.