Dekker1/TCP-setup-uppaal
Archived
1
0
Fork 0
Code

Bit cleaner without contractions

Browse Source
This commit is contained in:
Ben Brücker 2014-02-04 21:24:08 +01:00
parent 2e4b27b54a
commit 2d7eef99f2
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Report/GDN.tex
View File

@ -211,9 +211,9 @@ When a packet is accepted, then the ack that this host will send is set to the r
A[] not ((Host1.Closed or Host1.Listen
or Host1.SynSent) and Host2.Established)
\end{verbatim}
This query states that there isn't a state were Host1 is in the Closed, Listen or SynSent state while Host2 is in the Established state. Note that Host1 can be in the SynRcvd state while the other has an established connection. This would mean the first host is waiting for the last packet sent by the second host.
This query states that there is not a state were Host1 is in the Closed, Listen or SynSent state while Host2 is in the Established state. Note that Host1 can be in the SynRcvd state while the other has an established connection. This would mean the first host is waiting for the last packet sent by the second host.
Finally we want to guarantee that the protocol doesn't have places were the hosts get stuck and can not progress to a new state. This phenomenon is a deadlock in this model, where there is a state where no any options to advance are available. To test this we need to make sure that our established state transitions back to itself, so it doesn't result in an deadlock. Then we can check for deadlocks using the simple query:
Finally we want to guarantee that the protocol does not have places were the hosts get stuck and can not progress to a new state. This phenomenon is a deadlock in this model, where there is a state where no any options to advance are available. To test this we need to make sure that our established state transitions back to itself, so it does not result in an deadlock. Then we can check for deadlocks using the simple query:
\begin{verbatim}
A[] not deadlock
\end{verbatim}
@ -229,7 +229,7 @@ or Host1.SynSent) and Host2.Established)
% subsection model_verification (end)
\subsection{Guaranteeing an connection} % (fold)
\label{sub:guaranteeing_an_connection}
The queries become more interesting when trying to analyse a specific aspect of the model. The aspect we are interested in is a guaranteed connection set-up. This means that when both hosts are able to set-up a connection and both hosts want a connection, the connection will always set-up. Hosts are only able to set-up a connection when they aren't in the Init or Closed state. To force the hosts to enter the other states we remove the transition from the Closed state back to itself and guarantee the host leaves the Closed state by making it an committed state. To make sure a hosts does not deny the connection set-up we remove the possibility for hosts to return to the closed state. With these changes to the model we can now write a query that checks if the model does guarantee a connection between the two hosts given that they both try or accept connection set-up.
The queries become more interesting when trying to analyse a specific aspect of the model. The aspect we are interested in is a guaranteed connection set-up. This means that when both hosts are able to set-up a connection and both hosts want a connection, the connection will always set-up. Hosts are only able to set-up a connection when they are not in the Init or Closed state. To force the hosts to enter the other states we remove the transition from the Closed state back to itself and guarantee the host leaves the Closed state by making it an committed state. To make sure a hosts does not deny the connection set-up we remove the possibility for hosts to return to the closed state. With these changes to the model we can now write a query that checks if the model does guarantee a connection between the two hosts given that they both try or accept connection set-up.
\subsubsection{Case 1: Basic three-way handshake}
First we prove that if the connection is not set-up using an simultaneous initiation, that there will always follow an connection between the two hosts. To check if this condition holds within our model we need to disable the possibility for the simultaneous initiation. We do this by removing the transition from the Listen state to the SynSent state and forcing within the query that one host visits the SynSent state, while the other visits the Listen state. To check if these conditions result in an established connection we use the following query: