Demand Access Protocol Design and Validation with SPIN

In order for distributed systems to communicate reliably engineers standardize on communication rules (or protocols). Unforeseen behavior in communication protocols can push faults up to applications resulting in uncontrollable systems and should not be tolerated. However, while most modern protocols undergo extensive testing, rigorous formal methods, such as model checking, are rarely used due to complexity and intractable state spaces. Nevertheless, starting formal validation early in the development cycle provides less-complexity, significantly smaller state spaces and can allow for full validation. As a side benefit early error detection and correction costs significantly less than redesigns later in a system´s life-cycle.This paper discusses the preliminary design and validation of the Demand Access Protocol (DAP) using the SPIN model checker. Using English language specifications and flow charts, the author developed a PROMELA (the language used by SPIN) specification and tested basic safety properties. Used correctly, a model checker can thoroughly validate complex systems and guarantee absence of fault conditions.