A validation model of the VMTP transport level protocol

Abstract

The implementation of protocols can be speed up by incorporating formally validated designs in documents that describe new protocols. Unfortunately, this seldom happens in practice. It is proposed that a formally validated model of a protocol be developed before an implementation is attempted. Although this may seem like additional work, this approach can potentially reduce development time because misconceptions are ruled out at an earlier stage. Protocol validation is an established field of research. The techniques are mature enough to allow routine industrial applications. Currently suitable case studies are needed to introduce these techniques to industry. In this paper we describe the development of a validation model of VMTP, a transaction-based protocol that was used as a basis to develop an interprocess communication facility for a microkernel. While the validation of a specific protocol is a one-time event, the development techniques are of more lasting value and are applicable to other protocols.