计算机网络协议的安全性与活性验证

The Verification of Safety and Liveness for Computer Network Protocols

计算机通信协议,或简称协议,是管理网络与分布式系统中各种元素(实体与进程)之间交互与通信的一套规则。协议是并行执行的,可能借助不可靠的传送介质进行通信,因此设计正确可靠的协议,对网络与分布式系统具有特别重要的意义。

In this paper, protocol verification for computer networks and its main methods are described. Key properties of protocols, which include safety and liveness, are formally defined using Z notation. Taking alternating bit protocol as an examaple, verification problem of safety and liveness is discussed.