A polynomial algorithm for gateway generation from formal specifications

Author

Kristol, David M. ; Lee, David ; Netravali, Arun N. ; Sabnani, Krishan

Author_Institution

AT&T Bell Lab., Murray Hill, NJ, USA

Volume

1

Issue

2

fYear

1993

fDate

4/1/1993 12:00:00 AM

Firstpage

217

Lastpage

229

Abstract

A systematic procedure that takes exponential time to synthesize protocol converters from formal specifications is presented. The algorithm proceeds in two steps: compute the largest common subset of services provided by the two mismatched protocols, and reduce the converter, retaining common services, without traversing the entire machine that represents the composition of the two mismatched protocols. In a number of cases, the converter can be constructed by a memoryless translation of messages from one protocol to another. Conditions under which such stateless conversion is possible are given. Two examples are presented to illustrate the techniques. In the first example, a converter that interconnects a half-duplex protocol with a full-duplex protocol from their formal specifications is computed. In the second example, the polynomial procedure is applied to computation of a converter for interconnecting the SNR and TCP protocols

Keywords

formal specification; internetworking; polynomials; protocols; telecommunications computing; SNR/TCP interconnection; formal specifications; full-duplex protocol; gateway generation; half-duplex protocol; memoryless message translation; polynomial algorithm; protocol converters synthesis; stateless conversion; Access protocols; Application software; Computer architecture; Computer networks; Formal specifications; Integrated circuit interconnections; Network synthesis; Polynomials; Standards organizations; Sun;

fLanguage

English

Journal_Title

Networking, IEEE/ACM Transactions on

Publisher

ieee

ISSN

1063-6692

Type

jour

DOI

10.1109/90.222928

Filename

222928