Automated verification of a parametric real-time program: The ABR conformance protocol

Abstract

The ABR conformance protocol is a real-time program developed at France Telecom, that controls dataflow rates on ATM networks. A crucial part of this protocol is the dynamical computation of the expected rate of data cell emission. We present here a modelization of the corresponding program, using parametric timed automata. In this framework, a fundamental property of the service provided by the protocol to the user is expressed as a reachability problem. The tool HyTech is then used for computing the set of reachable states of the model, and automatically proving the property. This case study gives additional evidence of the importance of the model of parametric timed automata and the practical usefulness of symbolic analysis tools.