LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
4.00, Tuesday 29th April 1997

Title: The Bounded Retransmission Protocol Must be on Time!

Speaker: Joost-Pieter Katoen (University of Erlangen, Germany)

The bounded retransmission protocol (BRP), a protocol developed by Philips dedicated for communication between domestic equip- ment, has been (and still is) the subject of various verification efforts. Verifications using process algebras, I/O automata, theorem proving (PVS), and abstraction techniques have been carried out. These verifications consider the BRP in an untimed setting and focus on properties related to the correct transfer of data by the protocol. By making certain assumptions about the behaviour of the BRP the notion of time is neglected in these approaches.

In this talk we show that these assumptions are only valid if specific (non-trivial) dependencies are maintained between timer values in sender and receiver and (maximum) transmission delays. Using real-time model checking with UPPAAL we deduce tight timing constraints under which the BRP functions correctly. These time constraints are then used to justify an untimed specification of the BRP which is validated using the model checker SPIN.