dekker.one
An Uppaal analysis of the connection setup of the TCP protocol.
Changed TCP segment to TCP packet
+8
-8
Model/model.xml
+8
-8
Model/model.xml
···
18
18
bool ack;
19
19
SEQ seqNr;
20
20
SEQ ackNr;
21
-
} TCP_segment;
21
+
} TCP_packet;
22
22
23
-
void initialize(TCP_segment& p)
23
+
void initialize(TCP_packet& p)
24
24
{
25
25
p.seqNr := 0;
26
26
p.ackNr := 0;
···
28
28
p.ack := false;
29
29
}
30
30
31
-
meta TCP_segment to_network;
32
-
meta TCP_segment from_network;</declaration><template><name>Network</name><parameter>const int network</parameter><declaration>int target; // the target for the current network packet
33
-
meta TCP_segment transfer;
31
+
meta TCP_packet to_network;
32
+
meta TCP_packet from_network;</declaration><template><name>Network</name><parameter>const int network</parameter><declaration>int target; // the target for the current network packet
33
+
meta TCP_packet transfer;
34
34
clock c;
35
35
int packets_lost := 0; // Max packets a network can lose.
36
36
···
46
46
void send_packet(){
47
47
from_network := transfer;
48
48
}
49
-
</declaration><location id="id0" x="-5312" y="-1536"><committed/></location><location id="id1" x="-5152" y="-1664"><name x="-5160" y="-1696">PacketLost</name><committed/></location><location id="id2" x="-5312" y="-1664"><name x="-5360" y="-1696">PacketInTransit</name></location><location id="id3" x="-5312" y="-1408"><name x="-5360" y="-1384">ReadyToReceive</name></location><init ref="id3"/><transition><source ref="id0"/><target ref="id2"/><label kind="assignment" x="-5296" y="-1560">initialize(from_network)</label><nail x="-5280" y="-1592"/></transition><transition><source ref="id0"/><target ref="id3"/><label kind="synchronisation" x="-5304" y="-1488">Packet[target]!</label></transition><transition><source ref="id2"/><target ref="id0"/><label kind="guard" x="-5384" y="-1624">c <= TTL</label><label kind="assignment" x="-5416" y="-1608">send_packet()</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="guard" x="-5296" y="-1664">packets_lost > 0</label><label kind="assignment" x="-5288" y="-1648">packets_lost--</label></transition><transition><source ref="id1"/><target ref="id3"/><nail x="-5152" y="-1408"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-5432" y="-1560">Packet[network]?</label><label kind="assignment" x="-5432" y="-1544">set_target(),
49
+
</declaration><location id="id0" x="-5312" y="-1536"><committed/></location><location id="id1" x="-5152" y="-1664"><name x="-5208" y="-1696">PacketLost</name><committed/></location><location id="id2" x="-5312" y="-1664"><name x="-5360" y="-1696">PacketInTransit</name></location><location id="id3" x="-5312" y="-1408"><name x="-5360" y="-1384">ReadyToReceive</name></location><init ref="id3"/><transition><source ref="id0"/><target ref="id2"/><label kind="assignment" x="-5296" y="-1560">initialize(from_network)</label><nail x="-5280" y="-1592"/></transition><transition><source ref="id0"/><target ref="id3"/><label kind="synchronisation" x="-5304" y="-1488">Packet[target]!</label></transition><transition><source ref="id2"/><target ref="id0"/><label kind="guard" x="-5384" y="-1624">c <= TTL</label><label kind="assignment" x="-5416" y="-1608">send_packet()</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="guard" x="-5296" y="-1664">packets_lost > 0</label><label kind="assignment" x="-5288" y="-1648">packets_lost--</label></transition><transition><source ref="id1"/><target ref="id3"/><nail x="-5152" y="-1408"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-5432" y="-1560">Packet[network]?</label><label kind="assignment" x="-5432" y="-1544">set_target(),
50
50
receive_packet(),
51
51
c:=0</label><nail x="-5440" y="-1408"/><nail x="-5440" y="-1664"/></transition></template><template><name>Host</name><parameter>const int local, const int remote, const int network</parameter><declaration>clock c;
52
52
SEQ snd_nxt = 0;
53
53
SEQ snd_ack = 0;
54
54
SEQ rcv_nxt = 0;
55
55
const int seg_len = 0;
56
-
TCP_segment retrans;
57
-
TCP_segment received;
56
+
TCP_packet retrans;
57
+
TCP_packet received;
58
58
59
59
bool receive_packet(){
60
60
if (from_network.syn) {