We present 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.
|Name||CTIT Technical Report Series|
|Publisher||University of Twente, Centre for Telematics and Information Technology (CTIT)|