Formal methods for protocol conversion

The first part of this dissertation deals with constructing protocol converters from conversion specifications. With two target protocols specified in the Communicating Finite State Machine (CFSM) model and information of semantically equivalent transition sequences provided also in the form of Finite State Machines (FSMs), we propose two different methods to construct protocol converters.;In the first method, we propose a modular method to construct protocol converters. Target protocols are first decomposed into distinct functions; functional converters are then constructed for each pair of compatible functions; finally, local functions are merged with functional converters to construct the final converter. The final converter contains a common subset of functions of the two protocols and functionalities specific to each protocol. The modular method proposed can help identify the common subset of functions needed and reduce the complexity in the converter construction process.;The second method proposes a parallel method for protocol conversion. In this method, two half-converters, each implemented in a half-gateway, are constructed to provide the conversion function. By inserting error-recovery transitions into the half-converters, the proposed conversion scheme can handle faulty links between the two half-gateways.;The second part of this dissertation pertains to constructing protocol converters from service specifications. With two target protocols specified in a state-transition model and with a required service specification given in the FSM model, a protocol converter is constructed to provide the required services. We propose to use a system graph to construct a protocol converter so that the converter constructed is guaranteed to provide the required services. Two methods are proposed to construct a protocol converter using the system graph methodology.;In the first method, a system graph is constructed from the target protocol specifications and the required service specification. A protocol converter is derived from the system graph such that the required services can be provided.;The second method constructs a converter from the system graph derived using the required service specification and the service specifications of the target protocols. A service converter and new service specifications for target protocols are derived. The new involved entities are then integrated with the service converter to derive the final protocol converter. (Abstract shortened with permission of author.).