Promela model with spin - duplicate message and corrupt message

Question

I have this promela code and I need to model message duplication and message corruption and also I need to add mechanisms to detect and cope with corrupted messages and duplicates message

from my reading, I found that I need to add new processes one to duplicate message and another one for message corruption. Also for detecting the duplicate, I need to add a sequential number and for corrupting, I need to add checksum. my skills in pormela couldn't help me to transfer this information to code. if you can help or know a useful website to help I will appreciate

chan linkA = [1] of {byte};
chan linkB = [1] of {byte};
proctype sender (chan link; byte first)
{ byte n=first;
do
:: n <= 10 -> link!n; n=n+2
:: else -> break
od
}
proctype receiver ()
{ byte m, totaleven, totalodd;
do
:: linkA?m -> totaleven=totaleven+m
:: linkB?m -> totalodd=totalodd+m
od
}
init
{
run sender (linkA,2);
run sender (linkB,1);
run receiver ()
}

Patrick Trentin Patrick Trentin · Accepted Answer · 2019-01-14T07:41:57

Since this looks like an exercise, instead of providing you with the correct solution, I'll try to just give you some hints.

message duplication: instead of sending the message once, add a branching option for sending the message twice, similar to this:
```
if
    :: channel!MSG(value, seq_no, checksum)
    :: channel!MSG(value, seq_no, checksum);
       channel!MSG(value, seq_no, checksum); // msg. duplication
    :: true; // msg. loss
fi
```
At the receiver side, you cope with duplication and loss by checking the seq_no value. When a message is duplicated, you discard it. When a (previous) message is missing, you discard (for simplicity) the current message and ask for the message with the desired seq_no to be sent again, like, e.g.,
```
channel!NACK(seq_no)
```
message corruption: compute the checksum first, then alter the content of value
```
checksum = (seq_no ^ value) % 2
select(value : 1 .. 100)
...
channel!MSG(value, seq_no, checksum);
```
The checksum is very simple, I don't think it matters for the purposes of the exercise. At the receiver side, you compute the checksum on the data you receive, and compare it with the checksum value in the message. If it is not okay, you ask that it is sent again.

Promela model with spin - duplicate message and corrupt message

1 Answers