dekker.one
An Uppaal analysis of the connection setup of the TCP protocol.
Host rename and uncomplete query (mailed Frits)
+11
-6
+7
-2
Model/model.q
+7
-2
Model/model.q
···
3
3
/*
4
4
5
5
*/
6
+
(not Host1.Closed and not Host2.Closed) --> Host1.Established
7
+
8
+
/*
9
+
10
+
*/
6
11
A[] not deadlock
7
12
8
13
/*
9
14
10
15
*/
11
-
E<> (Host1Handshake.Established and Host2Handshake.Established)
16
+
E<> (Host1.Established and Host2.Established)
12
17
13
18
/*
14
19
15
20
*/
16
-
A[] not (Host1Handshake.Closed and Host2Handshake.Established)
21
+
A[] not (Host1.Closed and Host2.Established)
+4
-4
Model/model.xml
+4
-4
Model/model.xml
···
48
48
}
49
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(),
50
50
receive_packet(),
51
-
c:=0</label><nail x="-5440" y="-1408"/><nail x="-5440" y="-1664"/></transition></template><template><name>Host_Handshake</name><parameter>const int local, const int remote, const int network</parameter><declaration>clock c;
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;
···
99
99
Network2 = Network(0);
100
100
Network3 = Network(0);
101
101
Network4 = Network(0);
102
-
Host1Handshake = Host_Handshake(1,2,0);
103
-
Host2Handshake = Host_Handshake(2,1,0);
102
+
Host1 = Host(1,2,0);
103
+
Host2 = Host(2,1,0);
104
104
105
-
system Network1, Network2, Network3, Host1Handshake,Host2Handshake;
105
+
system Network1, Network2, Network3, Host1,Host2;
106
106
</system></nta>