Formal Description and Analysis of a Bounded Retransmission Protocol

Radu Mateescu

Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia), pages 98-113, June 1996

Also available as INRIA Research Report RR-2965.

Abstract:

This paper reports about the formal specification and verification of a Bounded Retransmission Protocol (Brp) used by Philips in one of its products. We started with the descriptions of the Brp service (i.e., external behaviour) and protocol written in the muCRL language by Groote and van de Pol. After translating them in the Lotos language, we performed verifications by model-checking using the Cadp (Caesar/Aldebaran) toolbox. The models of the Lotos descriptions were generated using the Caesar compiler (by putting bounds on the data domains) and checked to be branching equivalent using the Aldebaran tool.
Alternately, we formulated in the ACTL temporal logic a set of safety and liveness properties for the Brp protocol and checked them on the corresponding model using our Xtl generic model-checker.

31 pages

PDF

PostScript