A Success Story of Verifying a Real Complex Protocol
The advance in protocol specification using Formal Description Techniques (FDTs) in recent years has opened up a new horizon for protocol development. Techniques for verifying communication protocols have progressed significantly in the past decade. These developments have long promised to make contributions to the development of protocols. However, they are seldom adopted by the industry and applied by academia to real applications of considerable size. Reports on the successes of verifying real complex protocols have been rare; and it is by the suitability of their industrial applications and the extent of their usage that FDTs will ultimately be judged. This article presents the success story of using an automated stool, PROTEAN, for verifying a real complex protocol, the ISO FTAM protocol. The formal specifications are first discussed, followed by the description of how the specifications are verified by PROTEAN, and finally, the verification results are reported. The merit of this article is the demonstration of how formal specification and protocol verification can be used to improve a real protocol. It aims to encourage more research devoted to real applications and also to make a case for increased industrial attention and support for formal method approach to protocol development.