Designed as a part of the Arjuna distributed operating system, the rel/REL protocol [1] provides a reliable atomic multicast service between stations connected by a network. Although these stations may suffer from failures (i.e., they can crash), the rel/REL multicast service should ensure that a message sent by a transmitter is appropriately broadcasted to several receivers.

This case-study was performed in 1991 at the Hewlett-Packard Laboratory in Bristol [2, 3]. A LOTOS description of the rel/REL protocol was produced (approx. 300 lines). Describing the rel/REL protocol in LOTOS proved to be straightforward. The difficult point in was to model the fact that a station may crash at any moment: this problem was solved using the disabling operator provided by LOTOS, which is perfectly appropriate for this purpose.

The service provided by the protocol is expressed by two properties: atomicity (meaning that either all receivers get the message, or none of them) and causality (the order of messages is preserved). To prove these properties, various correctness-preserving abstractions were made on the LOTOS description. On the basis of these abstractions, several labelled transition systems were generated using the CAESAR compiler, and assuling a finite number of stations.

The atomicity property was verified using temporal logic. The causality property was verified using comparison modulo safety equivalence.

The formal verification of the rel/REL protocol revealed ambiguities in the informal description of the protocol. Furthermore, it provided additional information to implementors: for instance, it showed that message queues are always of bounded size; the value of the upper-bound was discovered automatically.

More recently (in 1996-97), a new verification experiment was carried out: the use of compositional verification allowed to verify a larger version of the rel/REL protocol (i.e. with a greater number of stations) [4].

1. Santosh K. Shrivastava and Paul D. Ezhilchelvan. "rel/REL: A Family of Reliable Multicast Protocol for High-Speed Networks". Technical Report, University of Newcastle, Dept. of Computer Science, U.K., 1990.

2. Simon Bainbridge and Laurent Mounier. Specification and verification of a reliable multicast protocol. Technical Report HPL-91-163, Hewlett-Packard Laboratories, Bristol, U.K., October 1991.

3. Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodriguez, and Joseph Sifakis. A toolbox for the verification of LOTOS programs. In Lori A. Clarke, editor, Proceedings of the 14th International Conference on Software Engineering ICSE'14 (Melbourne, Australia), pages 246-259. ACM, May 1992. Available on-line from the CADP Web site in PDF or PostScript

4. Jean-Pierre Krimm and Laurent Mounier. "Compositional state space generation from LOTOS programs". In Ed Brinksma, editor, Proceedings of TACAS'97 (Tools and Algorithms for the Construction and Analysis of Systems), Enschede, The Netherlands, April 1997. Springer Verlag. Extended version with proofs available as Research Report VERIMAG RR97-01. Available on-line from the CADP Web site in PDF or PostScript

• http://cadp.inria.fr/ftp/demos/demo_08
• http://cadp.inria.fr/ftp/demos/demo_20