-> prng inclus

[hdrcouchot.git] / modelchecking.tex

diff --git a/modelchecking.tex b/modelchecking.tex
index 191941605c1da2ba65fcc9ddff3a7e7223eb2c60..2a7107fb10dc6778a549fd269346ece5a32d7e2e 100644 (file)
--- 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.