Hewlett-Packard (Bristol, UK),
LGI/IMAG (Grenoble, FRANCE)
CADP (Construction and Analysis of Distributed Processes)
Distributed Systems. Multicast Protocols.
324 lines of LOTOS.
Designed as a part of the Arjuna distributed operating system, the rel/REL protocol  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
655 avenue de l'Europe
F-38330 Montbonnot Saint-Martin
Tel: +33 4 76 61 52 24
Fax: +33 4 76 61 52 52
2, avenue de Vignate
tel : +(33) 4 76 63 48 52
fax : +(33) 4 76 63 48 50
E-mail : Laurent.Mounier@imag.fr
The LOTOS sources as well as explanations on the verification with CADP
are available on-line at:|
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies