The SUT

The reference implementation that we used is a Java executable that was generated automatically from an Uppaal .xml file.

The Uppaal state machines we created of the sender, channel M and the receiver are :

• sender

Fig. 2: SUT Model : ABP output          

• channel

Fig. 3: SUT Model : Channel Frame        

• receiver

Fig. 4: SUT Model : ABP Receiver