Modeling and analysis of temporal constraints in communication protocols

Reachability analysis is the most popular and the most used method in protocol validation. It consists in constructing a graph called reachability graph, describing the communication of communicating machines exchanging messages through fifo channels. The states and structure of this graph are then analysed according to given properties to validate the corresponding communication protocol. In this paper, we go from the communicating machines used in the classical reachability analysis, to design temporal communicating machines allowing to specify quantitative temporal aspects of communication protocols. A temporal reachability graph describing the global behaviour of temporal communicating machines is then defined. After that, we show how this graph can be used to analyse general properties of communication protocols submitted to temporal constraints and we establish several complexity results dealing with this approach.