summaryrefslogtreecommitdiffstats
path: root/notFinishedCode/Report/test.tex.backup
diff options
context:
space:
mode:
Diffstat (limited to 'notFinishedCode/Report/test.tex.backup')
-rw-r--r--notFinishedCode/Report/test.tex.backup28
1 files changed, 19 insertions, 9 deletions
diff --git a/notFinishedCode/Report/test.tex.backup b/notFinishedCode/Report/test.tex.backup
index c163e2f..43541a7 100644
--- a/notFinishedCode/Report/test.tex.backup
+++ b/notFinishedCode/Report/test.tex.backup
@@ -131,18 +131,23 @@ One can easyly apply the class just by correctly defining the parameters: port a
A timeout exception gets raised when the cell phone does not respond (i.e. when the cell phone enters a deadlock or delayed state.) We had used the serial port library inside of Python although we use USB cables to connect to our cell phones. One should
be aware that our USB cables create a virtual serial port. More details on class design and an example can be found on our project wiki \cite{wiki}.
\subsection{Client and Server model}
-\cite{socket}
-
+Our socket communication code is based on the example given in the Python socket manual \cite{socket}.
+We extended it into two classes, a client and a server class. We had used the TCP protocol to base our two classes on\footnote{TCP is reliable compared to UDP (i.e. transmitted packets get also delivered),
+packets are ordered when received and data are received in a stream (i.e. multiple packets can be read at once.)}.
+The Server class can be seen in the following figure. The server class is implemented to accept only local connections\footnote{More details are given in the section 7.1}.
+First we determine our IP address and then create the socket and listen only for the same IP address (a different IP address than the selected one cannot connect to the server.)
+One has to define the port on which the server object should listen.
+When receiving data one can easily define the timeout to be raised if data are not received in the timeout range.
\begin{figure}[ht!]
\centering
\includegraphics[width=97mm]{ServerHandlerClass.png}
- \caption[]{Result image showing working, defected and not tested subsystems}
+ \caption[]{Server class}
\end{figure}
-
+The client class can be seen in the following figure.
\begin{figure}[ht!]
\centering
\includegraphics[width=90mm]{ClientClass.png}
- \caption[]{Result image showing working, defected and not tested subsystems}
+ \caption[]{Client class}
\end{figure}
@@ -214,10 +219,13 @@ requirements on the system's behavior are specified; finally, the model
checker is run to check if the correctness properties hold for the model, and,
if not, to provide a counterexample: a computation that does not satisfy a
correctness property.'' \cite{spin}. We modeled our simple protocol in SPIN using
-a programming language called PROMELA \cite{spin}. Since PROMELA is similar to C it was
+the programming language PROMELA \cite{spin}. Since PROMELA is similar to C it was
not possible to ensure 100\% matching with Python but we had made the assumptions of it.
-We modeled both sides, server and client side. As well as the server side
-The verification results are listed here:
+We modeled both sides, server and client side. As well as the server side being a caller
+and a callee. It was important to find out if our protocol is deadlock or delayed state free.
+For more details our model can be found on our wiki project page with the PROMELA source code \cite{wiki}.
+We had built in a 50\% random probability that the call test will not be successful, to make the model even more
+realistic. Our protocol idea was deadlock free and the verification results prove it:
\begin{lstlisting}
(Spin Version 6.1.0 -- 2 May 2011)
+ Partial Order Reduction
@@ -241,7 +249,9 @@ unreached in proctype Client
(0 of 67 states)
pan: elapsed time 0 seconds
\end{lstlisting}
-
+After we had modeled the basic idea we had written the code that implements our idea. The Python code
+resembles some kind of a state machine which remembers the last state and what the next state should be in case
+of receiving corresponding message. Otherwise it enters the exit state and then the start state.
\clearpage
\newpage