About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Conference paper
Generation of proper adapters and converters from a formal service specification
Abstract
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.