|Final Report of the COST-247 Action|
FORMAL DESCRIPTION AND ANALYSIS OF A BOUNDED RETRANSMISSION PROTOCOL
|INRIA Rhone-Alpes / Dyade|
|655, avenue de l'Europe|
|38330 MONTBONNOT ST MARTIN|
|tel: +(33) 4 76 61 52 83|
|fax: +(33) 4 76 61 52 52|
This talk 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 mCRL 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.
This presentation has been given during the COST-247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia, June 17--19, 1996).
COST-247 Working Group(s): 1-2
This Page was prepared by Mark Jorgensen.