summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--notFinishedCode/Report/test.aux2
-rw-r--r--notFinishedCode/Report/test.log42
-rw-r--r--notFinishedCode/Report/test.pdfbin698250 -> 702639 bytes
-rw-r--r--notFinishedCode/Report/test.tex28
-rw-r--r--notFinishedCode/Report/test.tex.backup28
-rw-r--r--notFinishedCode/Report/test.tex~28
6 files changed, 78 insertions, 50 deletions
diff --git a/notFinishedCode/Report/test.aux b/notFinishedCode/Report/test.aux
index a73f014..f21fd70 100644
--- a/notFinishedCode/Report/test.aux
+++ b/notFinishedCode/Report/test.aux
@@ -16,7 +16,7 @@
\citation{socket}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces }}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Client and Server model}{7}}
-\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces }}{7}}
+\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces }}{8}}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces }}{8}}
\citation{beagleDataSheet}
\@writefile{toc}{\contentsline {section}{\numberline {5}Hardware design}{9}}
diff --git a/notFinishedCode/Report/test.log b/notFinishedCode/Report/test.log
index f9cb449..a8fba90 100644
--- a/notFinishedCode/Report/test.log
+++ b/notFinishedCode/Report/test.log
@@ -1,4 +1,4 @@
-This is pdfTeX, Version 3.1415926-1.40.10 (TeX Live 2009/Debian) (format=pdflatex 2011.9.27) 11 OCT 2011 14:52
+This is pdfTeX, Version 3.1415926-1.40.10 (TeX Live 2009/Debian) (format=pdflatex 2011.9.27) 12 OCT 2011 14:56
entering extended mode
%&-line parsing enabled.
**test.tex
@@ -310,6 +310,11 @@ File: dbClass.png Graphic file (type png)
File: serialPort.png Graphic file (type png)
<use serialPort.png>
[6 <./dbClass.png (PNG copy)>]
+LaTeX Font Info: External font `cmex10' loaded for size
+(Font) <9> on input line 136.
+LaTeX Font Info: External font `cmex10' loaded for size
+(Font) <5> on input line 136.
+
<ServerHandlerClass.png, id=31, 359.3425pt x 181.67876pt>
File: ServerHandlerClass.png Graphic file (type png)
@@ -317,55 +322,50 @@ File: ServerHandlerClass.png Graphic file (type png)
<ClientClass.png, id=32, 507.30705pt x 256.48764pt>
File: ClientClass.png Graphic file (type png)
<use ClientClass.png>
-[7 <./serialPort.png (PNG copy)> <./ServerHandlerClass.png (PNG copy)>]
-[8 <./ClientClass.png (PNG copy)>] <bb.jpg, id=40, 521.95pt x 516.93124pt>
+[7 <./serialPort.png (PNG copy)>] [8 <./ServerHandlerClass.png (PNG copy)> <./C
+lientClass.png (PNG copy)>] <bb.jpg, id=43, 521.95pt x 516.93124pt>
File: bb.jpg Graphic file (type jpg)
<use bb.jpg> [9
<./bb.jpg>] [10]
-<protocolCommunicationHandler.png, id=48, 2486.93823pt x 792.13588pt>
+<protocolCommunicationHandler.png, id=51, 2486.93823pt x 792.13588pt>
File: protocolCommunicationHandler.png Graphic file (type png)
<use protocolCommunicationHandler.png>
-<protocolCommunicationcControllerReceiver.png, id=49, 1808.16705pt x 766.62883p
+<protocolCommunicationcControllerReceiver.png, id=52, 1808.16705pt x 766.62883p
t>
File: protocolCommunicationcControllerReceiver.png Graphic file (type png)
<use protocolCommunicationcControllerReceiver.png>
-<protocolCommunicationcControllerCaller.png, id=50, 1808.16705pt x 766.62883pt>
+<protocolCommunicationcControllerCaller.png, id=53, 1808.16705pt x 766.62883pt>
File: protocolCommunicationcControllerCaller.png Graphic file (type png)
<use protocolCommunicationcControllerCaller.png> [11
<./protocolCommunicationHandler.png (PNG copy)> <./protocolCommunicationcContr
ollerReceiver.png (PNG copy)> <./protocolCommunicationcControllerCaller.png (PN
-G copy)>]
-LaTeX Font Info: External font `cmex10' loaded for size
-(Font) <9> on input line 225.
-LaTeX Font Info: External font `cmex10' loaded for size
-(Font) <5> on input line 225.
- [12]
-<sshTunnel.png, id=59, 696.6025pt x 152.57pt>
+G copy)>] [12]
+<sshTunnel.png, id=61, 696.6025pt x 152.57pt>
File: sshTunnel.png Graphic file (type png)
<use sshTunnel.png> [13
<./sshTunnel.png (PNG copy)>] [14] [15]
-LaTeX Font Info: Try loading font information for OMS+cmr on input line 388.
+LaTeX Font Info: Try loading font information for OMS+cmr on input line 398.
(/usr/share/texmf-texlive/tex/latex/base/omscmr.fd
File: omscmr.fd 1999/05/25 v2.5h Standard LaTeX font definitions
)
LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <9> not available
-(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 388.
+(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 398.
[16] [17] [18]
LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <12> not available
-(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 460.
+(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 470.
<resultsImage.png, id=81, 702.625pt x 431.6125pt>
File: resultsImage.png Graphic file (type png)
<use resultsImage.png>
[19 <./resultsImage.png (PNG copy)>] [20]
-LaTeX Font Info: Try loading font information for T1+cmtt on input line 484.
+LaTeX Font Info: Try loading font information for T1+cmtt on input line 494.
(/usr/share/texmf-texlive/tex/latex/base/t1cmtt.fd
@@ -382,8 +382,8 @@ Here is how much of TeX's memory you used:
36i,10n,45p,751b,1285s stack positions out of 5000i,500n,10000p,200000b,50000s
</home/refik/.texmf-var/font
s/pk/ljfour/jknappen/ec/ectt1200.600pk> </home/refik/.texmf-var/fonts/pk/ljfour
-/jknappen/ec/ecrm0600.600pk> </home/refik/.texmf-var/fonts/pk/ljfour/jknappen/e
-c/ecrm0800.600pk> </home/refik/.texmf-var/fonts/pk/ljfour/jknappen/ec/ecrm0900.
+/jknappen/ec/ecrm0900.600pk> </home/refik/.texmf-var/fonts/pk/ljfour/jknappen/e
+c/ecrm0600.600pk> </home/refik/.texmf-var/fonts/pk/ljfour/jknappen/ec/ecrm0800.
600pk> </home/refik/.texmf-var/fonts/pk/ljfour/jknappen/ec/ecti1200.600pk> </ho
me/refik/.texmf-var/fonts/pk/ljfour/jknappen/ec/ecsx1200.600pk> </home/refik/.t
exmf-var/fonts/pk/ljfour/jknappen/ec/ecrm1095.600pk> </home/refik/.texmf-var/fo
@@ -394,9 +394,9 @@ ur/jknappen/ec/ecsx1440.600pk> </home/refik/.texmf-var/fonts/pk/ljfour/jknappen
sr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmmi12.pfb></usr/share/te
xmf-texlive/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texmf-texlive
/fonts/type1/public/amsfonts/cm/cmsy9.pfb>
-Output written on test.pdf (21 pages, 698250 bytes).
+Output written on test.pdf (21 pages, 702639 bytes).
PDF statistics:
- 626 PDF objects out of 1000 (max. 8388607)
+ 634 PDF objects out of 1000 (max. 8388607)
0 named destinations out of 1000 (max. 500000)
56 words of extra memory for PDF output out of 10000 (max. 10000000)
diff --git a/notFinishedCode/Report/test.pdf b/notFinishedCode/Report/test.pdf
index 816602b..29e3752 100644
--- a/notFinishedCode/Report/test.pdf
+++ b/notFinishedCode/Report/test.pdf
Binary files differ
diff --git a/notFinishedCode/Report/test.tex b/notFinishedCode/Report/test.tex
index 6475dee..131abe8 100644
--- a/notFinishedCode/Report/test.tex
+++ b/notFinishedCode/Report/test.tex
@@ -131,18 +131,26 @@ 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. While testing the server class we had the problem to listen on the same port if it was closed and started again in less than 60 seconds. We got the error message: "Address already in use".
+This is not known as an error but rather an option to help the server to catch lost live packets.
+We solved the problem by setting the socket options with the \emph{SO\_REUSEADDR} parameter. This enabled us to get around the error when we tried to restart our server application and it would not start.
+Before solving the problem without using the socket parameter, we had another solution to get around this problem by killing the application running the port.
\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}
@@ -217,9 +225,9 @@ correctness property.'' \cite{spin}. We modeled our simple protocol in SPIN usin
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
+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)
@@ -244,7 +252,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
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
diff --git a/notFinishedCode/Report/test.tex~ b/notFinishedCode/Report/test.tex~
index 65dc84e..501dda6 100644
--- a/notFinishedCode/Report/test.tex~
+++ b/notFinishedCode/Report/test.tex~
@@ -131,18 +131,24 @@ 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. While testing the server class we had the problem to listen on the same port if it was closed and started again in less than 60 seconds. We got the error message: "Address already in use"
+We solved the problem by setting the socket options with the \emph{SO\_REUSEADDR} parameter. This enabled us to get around the error when we tried to restart our server application.
\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}
@@ -217,10 +223,10 @@ correctness property.'' \cite{spin}. We modeled our simple protocol in SPIN usin
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,
-Our protocol idea was deadlock free and the verification results are listed here:
+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
@@ -244,7 +250,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