Formal specification and analysis of DMI-an X-25 based protocol
Vijay Gehlot, Ivan Lee · 2003
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.>