PAR protocol. Verification of the MSC specification.

Let us consider an example of property verification for the HMSC specification of PAR protocol.

PAR protocol (Positive Acknowledgement with Retransmission) is the protocol in which the sender waits for a positive acknowledgement before advancing to the next data frame. Data transmission in this protocol is made in one direction. All data frames contain the 1-bit sequence number (0 or 1) in order that the sender and the receiver can distinguish arriving frames. At each instant of time, the receiver expects a particular sequence number next. Any arriving frame containing the wrong sequence number is rejected as a duplicate. When a frame containing the correct sequence number arrives, it is accepted. Then the receiver increments the expected sequence number (0 becomes 1 and 1 becomes 0) and sends an acknowledgement to the sender. For more detailed information about the protocol, please see the  book “Computers Networks” by A. Tanenbaum.

HMSC specification

Graphical representation of the HMSC specification is presented below. Textual representation of the specification can be found in the repository with the following link: msc_specification.

The MSC document Stop and Wait Protocol contains the data declarations and the names of (H)MSCs which are used in the specification.

The HMSC Stop-and-Wait describes the possible scenarios of PAR protocol and consists of the following reference MSCs:

1. Init describes a variable initialization for sender and receiver processes;
2. FailSendAck describes a frame loss during transmission from Sender to Receiver and a timeout event for Sender process;
3. FailAck describes a frame loss during transmission of acknowledgment from Receiver to Sender and a timeout event for Sender process;
4. SuccessSendAck describes a successful frame delivery to Receiver, a successful receipt of acknowledgment by Sender and a timer reset for Sender process;
5. Finish describes a termination of frame transmission by Sender and a check of transmitted data by Receiver.

The Init diagram describes an initialization phase of the protocol before entering the loop. After variable initialization each process can evaluate events from one of the next MSCs: FailSendAck, SuccessSendAck, FailAck and Finish. The choice of some diagram is based on the value of guarding conditions, placed at the beginning of each MSC. While the value of variable hasData is true, one of the scenarios FailSendAck, SuccessSendAck or FailAck can be executed. The false value of hasData means that there are no data to transmit by Sender process. In this case the only scenario Finish can be executed.

The diagrams FailSendAck, FailAck and SuccessSendAck depict the data transmission between Sender and Receiver. The transmitted data in the protocol are the sequence of integers from 1 to 5. Sender has a variable sbuffer containing data value to send. Receiver has a variable buffer to store data values of arriving frames. Sender remembers the sequence number of the next frame to send in nextFr and Receiver remembers the sequence number of the next frame expected in expcFr. After frame transmitting and starting the timer T1, Sender waits for something to happen. Three possibilities exist: the transmitted frame is lost (the message sFrame_fail in the MSC FailSendAck), the transmitted acknowledgement is lost (the message rFrame in the MSC FailAck), or acknowledgement frame is successfully arrived (the MSC SuccessSendAck).

It should be noted that the protocol specification uses special MSC elements intended for timer modeling (timer set, timeout and reset). So, in the resulting CPN a timer execution event is modeled by firing of a transition corresponding to the timer event.

If an acknowledgement not arrive to Sender, the timer T1 expires (see the MSCs FailSendAck and FailAck). In this case the buffer variable sbuffer and the sequence number nextFr are not changed, so that a duplicate can be sent to Receiver.

When a transmitted frame arrives at the Receiver (see the reference MSC ReceiveData), its sequence number is checked to see if it is a duplicate (the statement when (nextFr = expcFr)). If not, Receiver saves the buffer value in the res variable, which accumulates all transmitted data from Sender process, and updates the expcFr variable. Next an acknowledgement is generated by Receiver. Note that duplicate frames are not accepted by Receiver.

When an acknowledgement arrives at the Sender (see the MSC SuccessSendAck), Sender resets the timer T1 and checks the condition when (ack = nextFr). If acknowledgement is not duplicate, then there are two cases. If the full sequence of integers is transmitted (sbuffer >= 5), then the transmission process is stopped (hasData := false). Else Sender updates the variables sbuffer and nextFr to send them in the next frame.

When Sender has no data to send, the Finish diagram is allowed. It is intended for validation of the protocol termination. This MSC performs a check of two conditions. The first condition when (hasData = false) checks a successful termination of data transmission on the side of Sender process. The second condition when (res = 12345) checks correctness of the transmitted data on the side of Receiver process. Thus, the execution of the HMSC Stop-and-Wait ends at its end node if the postcondition stated in the MSC Finish is true.

Output CPN model

The HMSC specification described above has been transformed into CPN. The output net has a format compatible with the CPN Tools system and can be found in the repository with the following link: par_protocol_cpn.

The output CPN is a hierarchical because the input specification was defined by HMSC with MSC references. The prime module of the CPN model corresponding to the HMSC is presented below.

As we can see in the figure above, each MSC reference is represented by a substitution transition related to separate subnet (module of CPN) to preserve an original hierarchical structure of the input HMSC.

The graphical representations of other CPN submodules corresponding to the reference MSCs are presented at the following links: MscInit, MscFailSendAck, MscReceiveData, MscFailAck, MscSuccessSendAck, MscFinish.

It should be noted that in this concrete example of protocol to simplify the resulting CPN we consider message input events without buffers for transmitted variable values. In this case we assume that all transmitted data values are stored in the global variables available for both processes.

Verification

For the resulting net the following properties of proper behavior is formulated:

1. the absence of deadlocks;
2. all sent data must be received;
3. the sequence of the received data equals to the sequence of the sent data.

The property 1 means that the resulting CPN should not have dead markings, except the markings corresponding to the endpoint of the HMSC (place P_END of net StopAndWait). The token at the place P_END means a successful completion of data transmission and an absence of deadlocks.

The property 2 is specified by the LTL formula: G ( p_send() -> F p_receive() ), where p_send() and p_receive() are predicates described as follows.

bool p_send() {
    return ( P_Send1 == 1 or P_Send2 == 1 )
}
bool p_receive() {
    return ( P_Receive1 == 1 )
}

In the pseudocode above P_Send1 and P_Send2 are places from CPN MscInit and MscSuccessSendAck, P_Receive1 – the place from CPN MscReceiveData. The token at the places P_Send1 or P_Send2 (the statements P_Send[i] == 1) means the sending of a new non-duplicate message to Receiver. Thus p_send() is true if a new message will be sent to Receiver in the next frame. The token at the P_Receive1 place (the statement P_Receive1 == 1) means the arriving of non-duplicate message from Sender. The predicate p_receive() is true if a transmitted message is accepted by Receiver.

The property 3 for the resulting CPN can be formulated as follows: in the final state of CPN model where no available transitions to occur, the place P_END must contain a single token with the value 1`().

The analysis of the model properties was made in the CPN Tools (the property 1) and in the automated verification system based on SPIN and developed in IIS SB RAS (the properties 2 and 3). To reduce the state space of the resulting CPN we introduced an additional restriction on the protocol model without loss of generality: the frame number that can be lost during transmission is limited to 10.

All properties described above are satisfied for the PAR protocol model.

Copyright (c) 2014 by Sergey Chernenok. This work is licensed under Creative Commons Attribution-ShareAlike 3.0 Unported License.