Experience with Formal Specifications Using an Extended State Transition Model

Experience with the use of formal descriptions of communication services and protocols is described. The paper focuses on the experience of the authors with the extended state transition model which is proposed as a standard formal description technique (FDT) for the services and protocols in the OSI environment. The first part of the paper refers to various example specifications, including transport protocol and service specifications, and discusses the suitability of the specification method and possible extensions. In the remaining part, the use of such formal specifications during the phases of system design, implementation, and testing is described. Various approaches to protocol design validation, implementation, and assessment of implementations are discussed, with emphasis on the last point. The experience with several of these approaches is described in the paper, and further details may be found in the references.