Verification of ABR conformance protocol
The ABR conformance protocol is a real-time program designed by CNET
(Centre national d'Etudes des Télécommunications, Lannion, France) in
the framework of ATM network communications. This program controls the
dataflow rates and its crucial part is the dynamical computation of the
expected rate of data cells. Algorithm B' proposed by P. Rabadan (CNET)
computes an approximate value of this expected rate, which must be fair
to the user. A first correctness proof for algorithm B' appears in a CNET
report ("Correction of an algorithm for ABR conformance", Dec. 1996) by
J. F. Monin and F. Klay.
The description and modelization of this case study can be found in
Research Report LSV-98-12:
Automatic verification of a parametric
real-time program: the ABR conformance protocol.
The correctness property of algorithm B' is expressed as a reachability
problem, involving three parameters, and proved via the tool
HyTech.
The file ABR.hy
contains the system description and the analysis commands,
using HyTech input language.
The files ABR.log
and ABRpre.log
contain the outputs produced by running HyTech on the source file, with
forward and backward computation respectively.