Formal Description and Analysis of a Bounded Retransmission
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.
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.