On the Analysis of Time-dependent Protocols by Network-flow Algorithms

A timed model for communication protocols is adopted, where finite-state machines augmented with (tmin, tmax) time labels communicate through the mechanism of coupled transitions. The model, called 'coupled time-graphs' (CT-graphs), supports the specification of timeouts, transmission delays and other time parameters of protocols for distributed systems. A two-phase analysis is proposed: the first phase generates system interactions, the second checks their time-consistency. An algorithm is given for the generative phase, which eliminates the problem redundantly computing all possible time orderings of a same set of concurrent events, with the inherent combinatorial explosion. For systems with linear or ring-like topology, the problem of checking time-consistency is shown to reduce, through a suitable graph transformation, to a network flow problem for which efficient algorithms are known. The two techniques have been integrated and implemented. Applications to a simple communication protocol with timeout are illustrated.