From d75d95aea7b8b7943704e181bfa0eaf9758da367 Mon Sep 17 00:00:00 2001
From: Refik Hadzialic
Date: Tue, 11 Oct 2011 14:54:02 +0200
Subject: Report writing!

---
 notFinishedCode/Report/test.tex | 54 +++++++++++++++++++++++++++++++++++------
 1 file changed, 46 insertions(+), 8 deletions(-)

(limited to 'notFinishedCode/Report/test.tex')

diff --git a/notFinishedCode/Report/test.tex b/notFinishedCode/Report/test.tex
index 8998141..6475dee 100644
--- a/notFinishedCode/Report/test.tex
+++ b/notFinishedCode/Report/test.tex
@@ -91,7 +91,7 @@ Prof. Dr. Gerhard Schneider\\ \vspace{1\baselineskip} Supervisors: \\ Konrad Mei
 \tableofcontents 
 
 %new page to start with 
-\newpage 
+\clearpage 
 
 
 
@@ -101,7 +101,7 @@ Prof. Dr. Gerhard Schneider\\ \vspace{1\baselineskip} Supervisors: \\ Konrad Mei
 \large In the following report, the authors will try to give you a brief insight into our team project. The goal of our project was to develop a mechanism for automatic testing of our University Telecommunication network. The Telecommunication network of University of Freiburg consists of: our own internal GSM and telephone network systems; GSM redirecting device (if one initiates a call to one of the four external GSM networks, it redirects the calls to: T-mobile, 02, Vodaphone or E-Plus); a SIP gateway for landline calls inside of Germany (sipgate.de) and international calls. Since we did not have access to internal servers, our strategy was to exploit the existing systems and infer the results out of our findings.
 Before we had started working on our project, we had to analyze the overall network to come up with test cases that contain the highest information content. The next step in our procedure was to implement our ideas into a working piece of software. 
 Gradually we implemented a bit-by-bit of the final software. Every single step was accompanied by testing and validation procedures. At the end we connected all the ``black-boxes'' into one big piece of software. We have fulfilled our requests and goals and made a fully working and operable test software. Despite developing a working software, all the way along we thought about the simplicity of the usage of the software. In the following chapters we will describe in more detail our approach and how each subsystem works.
-\newpage
+\clearpage
 \section{Requirements}           % chapter 2
 \newpage
 \section{Database design}
@@ -121,17 +121,32 @@ The method names are self-explanatory and do not require extra explanations. All
 Our first version of the developed program code for controlling the cell phones used predefined timed values
 to send commands instead of using a state controlled approach to confirm that every command was successfuly received and executed by the cell phone. 
 It meant we had to make an enormous number of assumptions. In comparison to our second approach, to build a state controlled cell phone control class,
-our first approach was inferior and slower. The state controlled method connected two cell phones, on the same base station, up to 15 times faster than timed approach. 
+our first approach was inferior and slower. The state controlled method connected two cell phones, on the same base station, up to 15 times faster than the timed approach. 
 \begin{figure}[ht!]
   \centering
   \includegraphics[width=80mm]{serialPort.png}
   \caption[]{GSM class diagram for controlling the cell phones}
 \end{figure}
-One can easyly apply the the class just by correctly defining the parameters: port address, baud rate and timeout. The former two are self-explanatory and the timeout parameter is used to define when the alarm function should raise a timeout exception. 
+One can easyly apply the class just by correctly defining the parameters: port address, baud rate and timeout. The former two are self-explanatory and the timeout parameter is used to define when the alarm function should raise a timeout exception. 
 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{subsection}
-\newpage
+\subsection{Client and Server model}
+\cite{socket}
+
+\begin{figure}[ht!]
+  \centering
+  \includegraphics[width=97mm]{ServerHandlerClass.png}
+  \caption[]{Result image showing working, defected and not tested subsystems}
+\end{figure}
+
+\begin{figure}[ht!]
+  \centering
+  \includegraphics[width=90mm]{ClientClass.png}
+  \caption[]{Result image showing working, defected and not tested subsystems}
+\end{figure}
+
+
+\clearpage
 \section{Hardware design}
 In our team project we had the option to choose all the required hardware ourself beside the two BeagleBoards, which we were supplied by Konrad and Dennis. 
 Since one of the project goals was to reduce the costs as much as it was possible, we had tried to use some of the leftovers found in our lab.
@@ -164,7 +179,11 @@ At the start we did not have a cable supplied for the Siemens S55 phone. We cont
 \subsection{Cables for the cell phones}
 Due to the fact that we had used 5 cell phones on a single computer, the best solution was to order 5 USB cables. 
 Konrad bought 5 cables for 5 Siemens S55 cell phones. All of the cables have an USB2Serial chip converter inside of them. 
-Once they were plugged into the USB port, Ubuntu automatically recognized the cables and it created properly virtual ports.
+Once they were plugged into the USB port, Ubuntu automatically recognized the cables and installed the drivers.
+The virtual serial ports were created and could be found on \emph{/dev/ttyUSBx}, where $x$ is the automatically assigned number for the port. 
+Some of the cables had the cability to charge the Siemens S55 phones. 
+Konrad had opened several cables to solder the power supplies to some contacts and the problem was solved for all of the cables. 
+
 \clearpage
 
 \section{Communication protocol}
@@ -188,7 +207,20 @@ Once they were plugged into the USB port, Ubuntu automatically recognized the ca
 \end{figure}
 
 \subsection{Verification of the protocol}
-The verification results are listed here:
+``SPIN is a model checker - a software tool for verifying models of physical
+systems, in particular, computerized systems. First, a model is written that
+describes the behavior of the system; then, correctness properties that express
+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
+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 being a caller 
+and a callee. It was important to find out if our protocol can be in a deadlock or delayed state. 
+For more details our model can be found on our wiki project page \cite{wiki}. 
+We had modeled also the chance that the call test was not successful, to make the model 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
@@ -453,7 +485,13 @@ If one of the fields is red it means the subsystem is not online or cannot be se
 
 \bibitem{wiki} \emph{[2011] GSM Selftest  - Wiki - Lehrstuhl f\"{u}r Kommunikationssysteme}, accessed on 20.09.2011, available at \\
 \url{http://lab.ks.uni-freiburg.de/projects/gsm-selftest/wiki}.
+
+\bibitem{socket} \emph{17.2. socket - Low-level networking interface}, accessed on 20.06.2011, available at 
+\url{http://docs.python.org/library/socket.html}.
  
+\bibitem{spin} M. Ben-Ari \emph{Principles of the Spin Model Checker},
+Springer Verlag, Weizmann Institute of Science, Israel, ISBN: 978-1-84628-769-5, 2008.
+
 \bibitem{sshTunnel} R. Natarajan, \emph{3 Steps to perform SSH login without password using ssh-keygen \& ssh-copy-id},  accessed on 18.08.2011, available at 
 \url{http://goo.gl/fX68N}.
 
-- 
cgit v1.2.3-55-g7522

