14th IEEE International Symposium on Modeling, Analysis, and Simulation
Verifying the Distributed Real-Time Network Protocol RTnet Using Uppaal
Monterey, CA
September 11-September 14
ISBN: 0-7695-2573-3
RTnet is a distributed real-time network protocol for fully-connected local area networks with a broadcast capability. It supports streaming real-time and non-realtime traffic and on-the-fly addition and removal of network nodes. This paper presents a formal analysis of RTnet using the model checker Uppaal. Besides normal protocol behaviour, the analysis focuses on the fault-handling properties of RTnet, in particular recovery after packet loss. Both qualitative and quantitative properties are presented, together with the verification results and conclusions about the robustness of RTnet.
Citation:
Ferdy Hanssen, Angelika Mader, Pierre G. Jansen, "Verifying the Distributed Real-Time Network Protocol RTnet Using Uppaal," mascots, pp.239-246, 14th IEEE International Symposium on Modeling, Analysis, and Simulation, 2006