Timed verification of the reliable adaptive multicast protocol

The uses of timed parameters in formalisms are important for providing realistic descriptions of distributed multimedia systems. We have developed Time-Estelle, an extended Estelle which is capable of doing so. Correct operations of this type of systems have stringent requirements for synchronisation of different entities or media data residing in a number of nodes possibly located very remotely from each other. Verification of formal specifications for such systems with time taken into consideration has been a subject of research. We have developed a method of verifying Time-Estelle specifications; it involves translating Time-Estelle specifications to Communicating Time Petri Nets which can then be verified by using the automated tool ORIS, with the dynamic behaviours of Estelle modules all supported. Using this verification method, this paper describes a timed verification of the Reliable Adaptive Multicast Protocol formally specified in Time-Estelle, and presents the results of the verification. Its contribution is that it represents a success in the use of a method in verifying a real-life protocol with timed properties specified formally.