PERFORMANCE SPECIFICATION AND LIVELOCK DETECTION/CORRECTION OF A PROTOCOL USING TIMED PETRI NETS

摘要

Models which abstract away the notion of time are not adequate to fully specify systems whose behavior depends on their temporal characteristics. Communication protocols fall into this category. In addition to their functional correctness, one must specify and verify their performance properties. Also, to some extent, the functional correctness depends on the timing characteristics of the system.In this paper we use Timed Petri nets to detect a livelock situation in a protocol which arises because of improper timer value. We then derive a necessary condition that the system parameters must satisfy to avoid such situation.We also illustrate the use of Timed Petri nets in formal performance specification of protocols.