Synthesis methods for the design and validation of communication protocols.

Communication protocol design consists essentially of the construction of interacting protocol entities which cooperate to provide a set of specified services to the service users. Protocol validation or design verification is a pre-implementation phase in the protocol development process which is essential for the detection of design errors such as deadlocks and incompleteness (unspecified receptions). The conventional analytic approach to protocol design consists of iteratively specifying a protocol in an informal manner, then validating it by analytic methods and correcting it until it becomes error-free. The synthetic approach consists of the automatic or semi-automatic (interactive) construction of the communicating protocol entities using a synthesis method which guarantees the correctness of the resulting protocol with respect to freedom from design errors and provision of the specified service. In this thesis, we develop service-oriented synthesis methods for the design and validation of communications protocols. First, we introduce an efficient, localized, synthetic technique for the validation of an existing protocol design. The technique can also be extended to complete an erroneous protocol design so as to satisfy the service specification. Then, after providing the rationale for designing protocols starting from service specifications, we introduce an automatic, service-oriented synthesis method for the design of communication protocols. Given the services a protocol is supposed to provide to a number of service users, our method automatically derives the specification of the corresponding communicating protocol entities. Both service and protocol entity specifications are modeled by the finite state machine (FSM) specification model. The interactions among the derived entities through a reliable FIFO communication medium combine to provide the set of specified services. Moreover, the synthesis method guarantees both semantic and syntactic correctness of the resulting protocol specifications. Furthermore, to enhance the expressive power of the specification model and the functionality of the protocol, the FSM model is extended to allow the specification to include concurrent behaviors of service users at the distributed service access points. The synthesis method is modified accordingly to accommodate this extended FSM specification model of communication services and protocols. This provides a potentially useful link to state-oriented FDTs (Formal Description Techniques) such as SDL (CCITT 88) and Estelle (ISO 9074). Moreover, the method is extended to synthesize error-recovery mechanisms in the derived protocol specifications to handle the case of an unreliable communication medium. Finally, the feasibility and usefulness of the synthesis method is demonstrated by its application to ISO's association control service specification. Interestingly, the method exactly reproduces the corresponding ISO protocol, thus providing evidence of the value of our approach for real protocol design processes