X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/f4997f36924772119b653509ff5ae4e8aef4200a..02fd942d6a30fe7197b732c94450ca466b7a49f5:/modelchecking.tex?ds=sidebyside

diff --git a/modelchecking.tex b/modelchecking.tex
index 1919416..2a7107f 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,6 +1,4 @@
 
-
-
 L'Ã©tude de convergence de systÃ¨mes dynamiques discrets est simple Ã  vÃ©rifier 
 pratiquement pour le mode synchrone. Lorsqu'on introduit des stratÃ©gies 
 pseudo pÃ©riodiques pour les modes unaires et gÃ©nÃ©ralisÃ©es, le problÃ¨me 
@@ -43,7 +41,7 @@ Les thÃ©orÃ¨mes de correction et de complÃ©tude de la dÃ©marche
 sont ensuite donnÃ©s Ã  la (\Sec{sec:spin:proof}). 
 Des donnÃ©es pratiques comme la complexitÃ© et des synthÃ¨ses d'expÃ©rimentation
 sont ensuite fournies (\Sec{sec:spin:practical}). 
-
+Ce chapitre a fait l'objet du rapport~\cite{Cou10:ir}.
 
 
 
@@ -782,7 +780,7 @@ pour Ã©tablir un verdict.
           $\bot$ & 374 & 7.7s&
           $\bot$ & 370 & 0.51s \\
           \hline %\cline{2-13}
-          AC2D 
+          \cite{RC07}
           &$\bot$ & 2.5 & 0.001s  % RC07_async_mixed.spin
           &$\bot$ & 2.5 & 0.01s   % RC07_async_mixed_all.spin
           &$\bot$ & 2.5 & 0.01s   % RC07_async.spin
@@ -816,7 +814,7 @@ du graphe complet.
 
 
 L'exemple  \textit{RE} a Ã©tÃ© prouvÃ© comme universellement convergent.
-\JFC{statuer sur AC2D}
+%\JFC{statuer sur AC2D}
 Comme la convergence n'est dÃ©jÃ  pas Ã©tablie pour les itÃ©rations synchrones
 de~\cite{RC07}, il en est donc 
 de mÃªme pour les itÃ©rations asynchrones.
@@ -826,16 +824,13 @@ $\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ et dÃ©bute avec $x=(0,0)$.
 En raison de la dÃ©pendance forte entre les Ã©lÃ©ments
 de~\cite{BM99}, 
 $\delta_0$ est rÃ©duit Ã  1. Cela aboutit cependant Ã  $2^{100}$ 
-configurations dans le mode des itÃ©rations asynchrones.
-
-\JFC{Quid de ceci?}
-La convergence des itÃ©rations asynchrones de l'exemple~\cite{BCVC10:ir} n'est pas Ã©tablie 
-lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle.
+configurations dans le mode des itÃ©rations asynchrones, montrant les limites de
+l'approche.
 
 \begin{figure}
 \centering
 \includegraphics[scale=0.6]{images/RC07ce.eps}   
-\caption{Contre exemple de convergence pour~\ref{fig:RC07CE}} \label{fig:RC07CE}
+\caption{Contre exemple de convergence pour~~\cite{RC07}} \label{fig:RC07CE}
 \end{figure}
 
 
@@ -868,7 +863,17 @@ lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle.
 \section{Conclusion}
 \label{sec:spin:concl}
 
-
+L'idÃ©e principale de ce chapitre est que l'on peut, 
+pour des rÃ©seaux boulÃ©ens Ã  dÃ©lais bornÃ©s de  petite taille, obtenir 
+une preuve de la convergence ou de sa divergence et ce
+de maniÃ¨re automatique.  
+L'idÃ©e principale est de traduire le rÃ©seau en PROMELA et de laisser 
+le model checker Ã©tablir la preuve.
+Toute l'approche a Ã©tÃ© prouvÃ©e: le verdict rendu par a donc valeur de vÃ©ritÃ©.
+L'approche a cependant ses limites et ne peut donc pas Ãªtre 
+apliquÃ©e qu'Ã  des modÃ¨les simplifiÃ©s de programmes.
+La suite de ce travail consiste Ã  se focaliser sur les systÃ¨mes qui ne 
+convergent pas.
 
 
 
