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
+pseudo périodiques pour les modes unaires et généralisés, le problème
se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones
-et mixes prenant de plus en compte les délais.
+et mixtes prenant de plus en compte les délais.
Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement
ont déjà été présentées~\cite{BM99,BCV02}.
Cependant, comme ces implantations ne sont pas exhaustives, elles ne donnent un résultat
formel que lorsqu'elles fournissent un contre-exemple. Lorsqu'elles exhibent une convergence,
-cela ne permet que donner une intuition de convergence, pas une preuve.
+cela ne permet que de donner une intuition de convergence, pas une preuve.
Autant que nous sachions, aucune démarche de preuve formelle automatique
de convergence n'a jamais été établie.
Dans le travail théorique~\cite{Cha06}, Chandrasekaran a montré que les itérations asynchrones sont convergentes
automatique pour construire cette fonction.
Un outil qui construirait automatiquement toutes
-les transitons serait le bienvenu.
+les transitions serait le bienvenu.
Pour peu qu'on établisse la preuve de correction et de complétude de la
démarche, la convergence du réseau discret ne reposerait
alors que sur le verdict
de quotientage selon une relation d'équivalence.
Ce chapitre montre comment nous simulons
-des réseaux discrets selon pour établir
+des réseaux discrets pour établir
formellement leur convergence (ou pas).
Nous débutons par un exemple et faisons quelques rappels sur
le langage PROMELA qui est le langage du model-checker
stratégie pseudo périodique, on a des comportements qui dépendent
de la configuration initiale:
\begin{itemize}
-\item initialisée avec 7, les itérations restent en 7;
-\item initialisée avec 0, 2, 4 ou 6 les itérations convergent vers 2;
+\item initialisées avec 7, les itérations restent en 7;
+\item initialisées avec 0, 2, 4 ou 6 les itérations convergent vers 2;
\item initialisées avec 1, 3 ou 5, les itérations convergent vers un des
deux points fixes 2 ou 7.
\end{itemize}
Il définit:
\begin{itemize}
\item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le nombre
- ${\mathsf{N}}$ d'éléments et le délais maximum $\delta_0$;
+ ${\mathsf{N}}$ d'éléments et le délai maximum $\delta_0$;
\item les deux tableaux (\verb+X+ et \verb+Xp+) de \verb+N+ variables booléennes;
les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associées à la variables $x_{i+1}$
d'un système dynamique discret;
elles mémorisent les valeurs de $X_{i+1}$ respectivement avant et après sa mise à jour;
-il suffit ainsi de comparer \verb+X+ et \verb+Xp+ pour constater si $x$ à changé ou pas;
+il suffit ainsi de comparer \verb+X+ et \verb+Xp+ pour constater si $x$ a changé ou pas;
\item le tableau \verb+mods+ contient les éléments qui doivent être modifiés lors de l'itération
en cours; cela correspond naturellement à l'ensemble des éléments $s^t$;
\item le type de données structurées \verb+vals+ et le tableau de tableaux
\item un canal \verb+sent+ qui vise à mémoriser \verb+d_0+ messages de type
\verb+bool+; le tableau nommé \verb+channels+ de \verb+N+*\verb+N+
éléments de type \verb+a_send+ est utilisé pour mémoriser les valeurs intermédiaires $x_j$;
- Il permet donc de temporiser leur emploi par d'autres elements $i$.
+ Il permet donc de temporiser leur emploi par d'autres éléments $i$.
\item les deux canaux \verb+unlock_elements_update+ et \verb+sync_mutex+ contenant
-chacun un message booléen et utilisé ensuite comme des sémaphores.
+chacun un message booléen et sont utilisés ensuite comme des sémaphores.
\end{itemize}
\end{xpl}
\begin{enumerate}
\item elle commence en mettant à jour la variable \texttt{X} avec les valeurs de \texttt{Xp} dans la fonction \texttt{update\_X},~\Fig{fig:spin:sauve}
-\item elle mémorise dans \texttt{Xd} la valeurs disponible pour chaque élément grâce à la fonction \texttt{fetch\_values}; cette fonction est détaillée
+\item elle mémorise dans \texttt{Xd} la valeur disponible pour chaque élément grâce à la fonction \texttt{fetch\_values}; cette fonction est détaillée
dans la section suivante;
\item une boucle %sur les \texttt{ar\_len} éléments qui peuvent être modifiés
met à jour itérativement la valeur de $j$ (grâce à l'appel de fonction \texttt{f(j)})
Cette section montre comment les délais inhérents au mode asynchrone sont
traduits dans le modèle PROMELA grâce à deux
fonctions \verb+fetch_values+ et \verb+diffuse_values+.
-Celles-ci sont données en {\sc Figure}~\ref{fig:val} et~\ref{fig:broadcast},
-qui récupèrent et diffusent respectivement les valeurs des elements.
+Celles-ci sont données en {\sc Figure}~\ref{fig:val} et~\ref{fig:broadcast}.
+Elles récupèrent et diffusent respectivement les valeurs des éléments.
\begin{figure}[t]
\begin{minipage}[h]{.475\linewidth}
\begin{itemize}
\item puisque $i$ connaît sa dernière valeur (\textit{i.e.}, $D^t_{ii}$ est toujours $t$)
\verb+Xd[i].v[i]+ est donc \verb+Xp[i]+;
-\item sinon, il y a deux sous cas qui peuvent peuvent potentiellement modifier la valeur
+\item sinon, il y a deux sous-cas qui peuvent peuvent potentiellement modifier la valeur
que $j$ a de $i$ (et qui peuvent être choisies de manière aléatoire):
\begin{itemize}
\item depuis la perspective de $j$ la valeur de $i$ peut ne pas avoir changé (
\diamond (\Box \verb+Xp+ = \verb+X+)
\label{eq:ltl:conv}
\end{equation}
-où les opérateur $\diamond$ et $\Box$ ont
+où les opérateurs $\diamond$ et $\Box$ ont
la sémantique usuelle, à savoir
respectivement {\em éventuellement} et {\em toujours} dans les chemins suivants.
On note que cette propriété, si elle est établie, garantit
et $\psi$ sa traduction en PROMELA. Le nombre de configurations
de l'exécution en SPIN de $\psi$ est bornée par $2^{m(\delta_0+1)+n(n+2)}$.
\end{theorem}
-\begin{Proof}
+\begin{proof}
Une configuration est une évaluation des variables globales.
Leur nombre ne dépend que de celles qui ne sont pas constantes.
$m$ et $\delta_0$.
%\JFC{Donner un ordre de grandeur de cet ordre de grandeur}
-\end{Proof}
+\end{proof}
La méthode détaillée ici a pu être appliquée sur l'exemple
pour prouver formellement sa convergence universelle.
On peut remarquer que SPIN n'impose l'équité faible qu'entre les process
alors que les preuves des deux théorèmes précédentes reposent sur le fait que
-celle-ci est établie dès qu'un choix indéterministe est effectué.
+cette équité est établie dès qu'un choix indéterministe est effectué.
Naïvement, on pourrait considérer comme hypothèse la formule suivante
chaque fois qu'un choix indéterministe se produit entre $k$ événements
respectivement notés $l_1$, \ldots $l_k$:
\begin{tabular}{|*{13}{c|}}
\cline{2-13}
\multicolumn{1}{c|}{ }
- &\multicolumn{6}{|c|}{Mode Mixe} & \multicolumn{6}{|c|}{Seulement borné} \\
+ &\multicolumn{6}{|c|}{Mode Mixte} & \multicolumn{6}{|c|}{Seulement borné} \\
\cline{2-13}
\multicolumn{1}{c|}{ }
&\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Pseudo-Périodique} &
\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
+pour des réseaux boolé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é.
+Toute l'approche a été prouvée: le verdict rendu par l'approche
+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
