FORMAL DESCRIPTION TECHNIQUES AT WORK - AN ISDN Q.931 IMPLEMENTATION USING LOTOS

This paper describes the formal specification, testing, and implementation of the D-channel layer 3 signalling protocol used in the user-network interface of the Integrated Services Digital Network. This protocol is informally defined in the CCITT Recommendation Q.931. The Formal Description Technique LOTOS has been used to formalize a subset of this definition, and to derive a Q.931 protocol implementation in C language, using semi-automatic tools. The resulting Q.931 implementation has been successfully integrated in a prototype Integrated Services Private Branch Exchange, developed in the ESPRIT Project DAMS (Dynamically Adaptable Multi-Service System). The aim of the work reported in this paper was not to find yet another protocol example, specify it in LOTOS, and see how easy or difficult it was, but rather to use LOTOS as an industrial tool to solve a specific problem. In the DAMS project we had to implement a protocol entity starting from a CCITT Recommendation, Q.931 in this case, and simply chose LOTOS as a convenient way for us to do it. The paper reflects our experiences in the different steps of the Q.931 development process, from the formal specification to the implementation in a real environment, trying to draw general conclusions and guidelines in order to evaluate the usage of LOTOS in other applications of similar characteristics.