Title :
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
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;
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
DOI :
10.1109/INFCOM.1988.12975
