We present the formal verification of a multicast protocol for mobile computing. The protocol supports reliable and totally ordered communication within a set of processes running on mobile hosts. Mobile hosts communicate with a wired infrastructure through wireless links. The protocol is specified in Calculus of Communicating Systems and checked using the Concurrency Workbench tool. The protocol was chosen as a case study to evaluate the usefulness 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 property itself. The reduction is obtained by transforming the program into one having a smaller representation. The approach is based on a logic, the selective 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 truth value of the formula itself, and thus can be ignored. We show and discuss the experimental results obtained.
Efficient Verification of a Multicast Protocol for Mobile Computing
ANASTASI, GIUSEPPE;DE FRANCESCO, NICOLETTA;
2001-01-01
Abstract
We present the formal verification of a multicast protocol for mobile computing. The protocol supports reliable and totally ordered communication within a set of processes running on mobile hosts. Mobile hosts communicate with a wired infrastructure through wireless links. The protocol is specified in Calculus of Communicating Systems and checked using the Concurrency Workbench tool. The protocol was chosen as a case study to evaluate the usefulness 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 property itself. The reduction is obtained by transforming the program into one having a smaller representation. The approach is based on a logic, the selective 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 truth value of the formula itself, and thus can be ignored. We show and discuss the experimental results obtained.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
