Modelling and analysis of the bounded-retransmission protocol: experience with discrete time in the LTSA

Abstract

The Bounded Retransmission Protocol is an industrial protocol designed for the transfer of large data files over unreliable communication lines. The protocol relies on specific assumptions on the timed behaviour of its components. This paper describes our experience with modelling and analysing the Bounded Retransmission Protocol using the LTSA. The LTSA uses labelled transition systems to specify behaviour, and compositional reachability analysis to incrementally generate, minimise, and analyse a system, based on its software ar-chitecture. The tool was not originally designed to deal with real-time applications. However, by modelling time as a discrete entity, the LTSA does not need to be extended in order to han-dle such systems. We discuss how the features of the tool can be exploited to model and ana-lyse behaviours that involve time.