Design and validation of protocols: a tutorial
It can be remarkably hard to design a good communications protocol, much harder than it is to write a 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 tuturial we introduce a state-of-the-art tool called SPIN and the specification language PROMELA. We show how the language and the tool can be used to design reliable protocols. The tool itself is available by anonymous ftp from research.att.com, or by email from the author.
원문보기 무료다운로드 유료다운로드
- 무료 원문 정보가 존재하지 않습니다.
NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니 담기를 통하여 원문복사서비스 이용이 가능합니다.