Consider the simple protocol CPN model discussed in the lectures.
Use the CPN Tools simulator to perform some interactive simulations (including manual binding of variables) and automatic simulations of the CPN model.
When an acknowledgement is received by the sender, it updates the counter on NextSend according to the sequence number contained in the acknowledgement. This implies that the counter on NextSend can be decreased when an "old" acknowledgement is received. Use the CPN simulator and interactive simulation to construct a scenario where this situation occurs.
Modify the CPN model such that the counter on NextSend will never be decreased. Use simulation to validate the modified model.
A demo of the editing facilities in CPN Tools will be given prior to the start of this exercise.
Consider the following variant of the stop-and-wait protocol where there is a limit on the number of packets that can be on the network at the same time.
The CPN model specifies no bound on the number of times that a data packet can be transmitted. Modify the CPN model such there is a bound on the number of times that a packet can be retransmitted.
Use simulation to validate the modified model.
A demo of the state space analysis facilities in CPN Tools will be given prior to the start of this exercise.
Investigate the correctness of this variant of the simple protocol developed in Exercise 2. Start by considering a small number of packets (2-3) to be transmitted and a small value of the retransmission limit (e.g., 2). The query functions ListDeadMarkings and HomeSpace might be useful.
Investigate the protocol for different values of the protocol parameters.
The simple protocol considered above is a stop-and-wait protocol: The sender keeps sending the same packet until the matching acknowledgement is received. In sliding window protocols, it is possible for the sender to transmit several packets to the receiver before receiving an acknowledgement.
Modify the CPN model such that it models a sliding window. For a first version, it should only be necessary to modify the Sender part of the CPN model.
Use simulation to validate the correctness of the protocol.
Use state space analysis to verify your sliding window protocol model. If you discover errors in your protocol, try to find a counter example and try also to fix any identified errors.