Using SPIN to verify protocols at the implementation level
Dirk Bull, Pieter de Villiers · South African Institute of Computer Scientists and Information Technologists · 2002
One way to improve the reliability of reactive systems is to use formal development methods. Although powerful techniques exist for verifying specifications, a remaining problem is to show that an implementation satisfies its specification.In this paper we describe a development method for improving the reliability of reactive systems, the main idea being to structure specifications as transition systems. In this way flow of control is formally separated from data manipulation which makes it possible to use a standard verification technique to check control flow at the implementation level. At the same time testing is simplified significantly. The alternating bit protocol is used to explain the proposed method. In addition, an implementation of the TCP protocol is discussed to illustrate that the technique is also applicable to reactive systems of realistic size and complexity.