文件名称：Tutorial: Design and Validation of Protocols
文件大小：142KB
文件格式：PDF
更新时间：2013-08-24 13:49:26
Design and Validation of Protocols
It can be remarkably hard to design a good communications protocol, much harder even than it is to write a normal sequential program. Unfortunately, when the design of a new protocol is complete, we usually have little trouble convincing ourselves that it is trivially correct. It can be a unreasonably hard to prove those facts formally and to convince also others. Faced with that dilemma, a designer usually decides to trust his or her instincts and forgo the formal proofs. The subtle logical flaws in a design thus get a chance to hide, and inevitably find the worst possible moment in the lifetime of the protocol to reveal themselves. Though few will admit it, most people design protocols by trial and error. There is a known set of trusted protocol standards, whose descriptions are faithfully copied in most textbooks, but there is little understanding of why some designs are correct and why others are not. To design and to analyze protocols you need tools. Until recently the right tools were simply not generally available. But that has changed. In this tutorial we introduce a state-of-the-art tool called SPIN and a specification language called PROMELA, and we show how these can be used to design reliable protocols.