Generation of proper adapters and converters from a formal service specification

An efficient approach is described for solving a protocol conversion problem by a formal method. It is assumed that protocol entities are modeled by automata and that the required services of the conversion system are known. It is shown that an adaptor can be generated if and only if an adaptor exists. A method for verifying the liveness of the conversion system is examined, and it is used to construct a proper converter that has desirable properties, such as bounded queues, and deadlock- and unspecified-reception-free properties, from a conversion system with an adapter.