Detection of Livelocks in Communication Protocols by Means of a Polygon Time Structure

As has been shown, the polygon time structure overcomes the main limitations of the interval time structure, and allows to verify communication protocols, in which the explicit concurrency of both competing and supporting events is considered. In this paper we have applied the polygon time structure to the verification of dynamic properties (like livelocks) of a simple protocol. As a result, we have shown that an application of the previously used interval time structure may lead to the evaluation of a protocol as incorrect, while it is livelock free.

• Type: Conference
• Year: 2000
• Where: SRDS
• Authors: Jerzy Brzezinski, Michal Sajkowski
• Keywords: Interval Time Structure, Operating Systems, Polygon Time Structure, SRDS 2000, Time Structure