Related publications: [AJUV13]
We consider the connection establishment and termination between Client and Server, but leave out the data transfer phase. As SUT, we consider the Server component of the protocol. We consider Request messages, which are input to the SUT, and Response messages, which are the output from the SUT. Messages in TCP are of form Request/Response(SYN,ACK,FIN,SeqNr,AckNr). Among parameters, SYN, ACK, and FIN are flags that define what type of message is sent: SYN synchronizes sequences numbers, ACK acknowledges the previous SeqNr, and FIN signals the end of the data transfer phase. SeqNr is a number that needs to be synchronized with both sides of the connection, and AckNr acknowledges a previous sequence number. Both Client and Server can send messages with the same parameters as defined above. We distinguish these messages by using Request for messages that are sent to the SUT and Response for messages that come from the SUT.
We used the protocol simulator ns-2 [ns2], which provides implementations of many protocols, to serve as System Under Test (SUT). As SUT, we consider the Server component of the protocol.
To define the mapper, we use information obtained from the standard RFC 793. For the flags SYN, ACK, and FIN, there are four valid combinations, shown in the first row of Table 1, thus defining four abstract values SYN, SYN+ACK, ACK, and ACK+FIN. The parameters SeqNr and AckNr are treated as sequence numbers. In this case, they will be incremented with each transmission round in a session. We therefore define four state variables: last_SeqNr_sent and last_AckNr_sent are the last values of SeqNr and AckNr, respectively, that have been transmitted to ns-2 in a valid Request message. last_SeqNr_recd and last_AckNr_recd are the last values of SeqNr and AckNr, respectively, that have been received from ns-2 in a valid Response message: they are initially undefined. By "VALID", we understand messages that follow the protocol and increment parameters SeqNr and AckNr appropriately. Using these state variables, the abstraction mappings for Request and Response messages are shown in the second and third part of Table 1. The main information is that in VALID messages, each AckNr increments the previously sent SeqNr at both sides, and that each SeqNr should be that of the previously received AckNr.
| Request | SYN | SYN+ACK | ACK | ACK+FIN |
| Type | SYN=1 | SYN=1 AND ACK=1 | ACK=1 | ACK=1 AND FIN=1 |
| Request | VALID | INVALID |
| SeqNr | SeqNr = last_AckNr_recd | SeqNr != last_AckNr_recd |
| AckNr | AckNr = last_SeqNr_recd + 1 | AckNr != last_SeqNr_recd + 1 |
| Response | VALID | INVALID |
| SeqNr | SeqNr = 0 OR SeqNr = last_AckNr_sent | SeqNr != 0 AND SeqNr != last_AckNr_sent |
| AckNr | AckNr = last_SeqNr_sent + 1 | AckNr != last_SeqNr_sent + 1 |
Table 1. Abstraction of parameters in input and output messages of TCP
Attach:TCP_server.pdf"Model of TCP Server" Fig. 1: Learned model of the TCP server. For readability, we write Flag(SeqNr,AckNr)/Flag'(SeqNr',AckNr') instead of Request(Flag,SeqNr,AckNr)/Response(Flag',SegNr',AckNr'). Moreover, V represents the VALID equivalence class and INV represents the INVALID equivalence class.