Efficient verification of a multicast protocol for mobile computing

We present the formal verification of a multicast protocol for mobile compu ting. The protocol supports reliable and totally ordered communication with in a set of processes running on mobile hosts. Mobile hosts communicate wit h a wired infrastructure through wireless links. The protocol is specified in Calculus of Communicating Systems and checked using the Concurrency Work bench tool. The protocol was chosen as a case study to evaluate the usefuln ess of a methodology, by means of which a property is checked on a reduced system, where the reduction is driven by the formula expressing the propert y itself. The reduction is obtained by transforming the program into one ha ving a smaller representation. The approach is based on a logic, the select ive mu-calculus, which has the characteristic that each formula allows the immediate pointing out of the parts of the system that do not alter the tru th value of the formula itself, and thus can be ignored. We show and discus s the experimental results obtained.