From formal specification to implementation: experience with protocol tools

The authors describe efforts to develop the Q.931 protocol software for the 5ESS Central Office Switch. Q.931 is a layer-3 message-based, user/network interface protocol for the integrated services digital network (ISDN). The approach uses a single formal specification written in the Augmented Protocol Specification Language to model the 1.931 protocol as a set of communicating extended finite state machines. From this specification, tools validate the protocol and generate the bulk of a C language implementation. The authors successfully integrated this code, along with other handwritten code, into a working system in the lab. Their results demonstrate that protocol tools can be used effectively to develop high quality protocol software quickly from formal specifications