Formal specification and analysis of DMI-an X-25 based protocol

Author

Gehlot, V. ; Lee, L.

Author_Institution

Dept. of Comput. Inf. Sci., Pennsylvania Univ., Philadelphia, PA, USA

fYear

1988

fDate

27-31 March 1988

Firstpage

641

Lastpage

650

Abstract

The digital multiplexed interface (DMI) specifies the interface requirements for multiplexed data communication over digital facilities between a host computer and a PBX. A part of the DMI´s packet-mode data-transfer protocol, which is based on the X.25 packet-level protocols, is specified formally using the selection/resolution (S/R) model. A formal verification of the resetting phase of this protocol, using the S/R-model-based software tool SPANNER, is presented. It is shown that the protocol is not fully correct in the sense that some sequence of events may lead it to unsafe states. These states give rise to a livelock situation. A way to rectify this problem is suggested.<>

Keywords

packet switching; protocols; DMI; PBX; SPANNER; X-25 based protocol; digital multiplexed interface; host computer; multiplexed data communication; packet-level protocols; selection/resolution model; Automata; Computer interfaces; Data communication; Formal specifications; Formal verification; ISDN; Information science; Reachability analysis; Software tools; Transport protocols;

fLanguage

English

Publisher

ieee

Conference_Titel

INFOCOM '88. Networks: Evolution or Revolution, Proceedings. Seventh Annual Joint Conference of the IEEE Computer and Communcations Societies, IEEE

Conference_Location

New Orleans, LA, USA

Print_ISBN

0-8186-0833-1

Type

conf

DOI

10.1109/INFCOM.1988.12975

Filename

12975