-\JFC{donner dans les rappels les délais et les propriétés de convergence universelle}
-\JFC{Statuer sur la taille des exemples traitables par la démarche, cf données pratiques}
-\section{Exemple jouet}
-\begin{xpl}
- On considère dans ce chapitre l'exemple où trois éléments dans $\Bool$.
- Chaque configuration est ainsi un élement de $\{0,1\}^3$, \textit{i.e.},
- un nombre entre 0 et 7.
- La \Fig{fig:map} précise la fonction $f$ considérée et
- la \Fig{fig:xplgraph} donne son graphe d'intéraction.
-
+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
+se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones
+et mixes 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.
+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
+si et seulement si on peut construire une fonction de Lyaponov décroissante, mais il ne donne pas de méthode
+automatique pour construire cette fonction.
+
+Un outil qui construirait automatiquement toutes
+les transitons 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 repose alors que sur le verdict
+donné par l'outil.
+Cependant, même pour des réseaux discrets à peu d'éléments,
+le nombre de configurations induites explose rapidement.
+Les \emph{Model-Checkers}~\cite{Hol03,nusmv02,Blast07,MCErlang07,Bogor03}
+sont des classes d'outils qui addressent le problème de vérifier automatiquement
+qu'un modèle vérifie une propriété donnée. Pour traiter le problème d'explosion
+combinatoire, ces outils appliquent des méthodes d'ordre partiel, d'abstraction,
+de quotientage selon une relation d'équivalence.
+
+Ce chapitre montre comment nous simulons
+des réseaux discrets selon toutes les sortes d'itérations 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
+SPIN~\cite{Hol03} (\Sec{sec:spin:promela}).
+Nous présentons ensuite la démarche de traduction
+de réseaux discrets dans PROMELA (\Sec{sec:spin:translation}).
+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}).
+
+
+
+
+
+
+
+%\section{Exemple jouet}
+
+
\begin{figure}[ht]
- \centering
- \begin{minipage}%[h]
- {.6\linewidth}
- \begin{center}
+ \begin{center}
+ \subfigure[Fonction à itérer]{
$ F(x)= \left \{
\begin{array}{rcl}
f_1(x_1,x_2,x_3) & = & x_1.\overline{x_2} + x_3 \\
\end{array}
\right.
$
- \end{center}
- \caption{Fonction à itérer} \label{fig:map}
- \end{minipage}
- \begin{minipage}%[h]
- {.35\linewidth}
- \begin{center}
+ \label{fig:map}
+ }
+ \hfill
+ \subfigure[Graphe d'intéraction]{
\includegraphics[width=4cm]{images/xplCnxMc.eps}
- \end{center}
- \caption{Graphe d'intéraction}
- \label{fig:xplgraph}
- \end{minipage}
+ \label{fig:xplgraph}
+ }
+ \end{center}
\caption{Exemple pour SDD $\approx$ SPIN.}
\end{figure}
+\begin{xpl}
+ On considère un exemple à trois éléments dans $\Bool$.
+ Chaque configuration est ainsi un élement de $\Bool^3$, \textit{i.e.},
+ un nombre entre 0 et 7.
+ La \Fig{fig:map} précise la fonction $f$ considérée et
+ la \Fig{fig:xplgraph} donne son graphe d'intéraction.
+
+
+
-On peut facilement vérifier que toutes les itérations parallèles initialisées
+
+On peut facilement vérifier que toutes les itérations synchrones initialisées
avec $x^0 \neq 7$ soit $(111)$
convergent vers $2$ soit $(010)$; celles initialisées avec
$x^0=7$ restent en 7.
-Pour les autres modes synchrones avec une
-stratégie pseudo périodique, les comportements selon la configuration initiale:
+Pour les mode unaires ou généralisés avec une
+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;
\end{figure}
-Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
-\texttt{short} et \texttt{int}. Comme dans le langage C par exemple,
-on peut déclarer des tableaux à une dimension de taille constante
+% Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
+% \texttt{short} et \texttt{int}.
+Comme en C,
+on peut déclarer des tableaux à une dimension
ou des nouveaux types de données (introduites par le mot clef
-\verb+typedef+). Ces derniers sont utilisés pour définir des tableaux à deux
-dimensions.
+\verb+typedef+). % Ces derniers sont utilisés
+% pour définir des tableaux à deux
+% dimensions.
\begin{xpl}
Le programme donné à la {\sc Figure}~\ref{fig:arrayofchannels} correspond à des
-déclarations de variables qui serviront dans l'exemple jouet de ce chapitre.
-Il définit tout d'abord:
+déclarations de variables qui servent dans l'exemple de ce chapitre.
+Il définit:
\begin{itemize}
\item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le nombre
$n$ d'éléments et le délais 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
-(le décalages d'un entier est dû à l'indexation à partir de zéro des cellules d'un tableau);
-Elles mémorisent les valeurs de $X_{i+1}$ respectivement avant et après sa mise à jour;
+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;
\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
\verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise à mémoriser $x_{j+1}^{D^{t-1}_{i+1j+1}}$
- pour l'itération au temps $t$ (en d'autres termes, utile lors du calcul de $x^{t}$).
+ pour l'itération au temps $t$.
+%(en d'autres termes, utile lors du calcul de $x^{t}$).
\end{itemize}
-Puisque le décalage d'un indices ne change pas fondamentalement
-le comportement de la version PROMELA par rapport au modèle initial
-et pour des raisons de clarté, on utilisera par la suite la même
-lettre d'indice entre les deux niveaux (pour le modèle: $x_i$ et pour PROMELA:
-\texttt{X[i]}). Cependant, ce décalage devra être conservé mémoire.
+% Puisque le décalage d'un indices ne change pas fondamentalement
+% le comportement de la version PROMELA par rapport au modèle initial
+% et pour des raisons de clarté, on utilisera par la suite la même
+% lettre d'indice entre les deux niveaux (pour le modèle: $x_i$ et pour PROMELA:
+% \texttt{X[i]}). Cependant, ce décalage devra être conservé mémoire.
-Une donnée de type \texttt{channel} permet le
+Déclarée avec le mot clef \verb+chan+,
+une donnée de type \texttt{channel} permet le
transfert de messages entre processus dans un ordre FIFO.
-Elles serait déclarée avec le mot clef \verb+chan+ suivi par sa capacité
-(qui est constante), son nom et le type des messages qui sont stockés dans ce canal.
+% Elles serait suivi par sa capacité
+% (qui est constante), son nom et le type des messages qui sont stockés dans ce canal.
Dans l'exemple précédent, on déclare successivement:
\begin{itemize}
-\item un canal \verb+sent+ qui vise à mémoriser\verb+d_0+ messages de type
+\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$.
%\subsection{PROMELA Processes}
Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurrence
-au sein de systèmes. Un process est déclaré avec le mot-clé
-\verb+proctype+ et est instancié soit immédiatement (lorsque sa déclaration est préfixée
+au sein de systèmes. Un process est instancié soit immédiatement
+(lorsque sa déclaration est préfixée
par le mot-clef \verb+active+) ou bien au moment de l'exécution de l'instruction
\texttt{run}.
Parmi tous les process, \verb+init+ est le process initial qui permet
La mise à jour de l'ensemble $s^t=\{s_1,\ldots, s_m\}$ des éléments qui constituent la stratégie
$(s^t)^{t \in \Nats}$ est implantée à l'aide du process \verb+update_elems+ fourni à la
{\sc Figure}~\ref{fig:proc}.
-Ce process actif attend jusqu'à ce qu'il soit débloqué par le process
+Ce processus actif attend jusqu'à ce qu'il soit débloqué par le process
\verb+scheduler+ à l'aide du sémaphore \verb+unlock_elements_update+.
L'implantation se déroule en cinq étapes:
L'introduction de l'indéterminisme à la fois dans les fonctions \verb+fetch_values+
et \verb+diffuse_values+ est nécessaire dans notre contexte. Si celui-ci n'était
-présent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple récupérer *
+présent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple récupérer
la valeur $x_i^{(t)}$ sans considérer la valeur $x_i^{(t-1)}$.
De manière duale, si le non déterminisme était uniquement
utilisé dans la fonction \verb+diffuse_values+, alors chaque fois qu'une valeur serait
annexes~\ref{anx:promela}.
-\begin{theorem}[Correction]\label{Theo:sound}
+\begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
+\label{Theo:sound}
+%
Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.
Si $\psi$ vérifie
la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible, alors
les itérations de $\phi$ sont universellement convergentes.
-\end{theorem}
+\end{restatable}
-
-\begin{theorem}[Complétude]\label{Theo:completeness}
+\begin{restatable}[Complétude de la traduction vers Promela]{theorem}{promelacomplete}
+\label{Theo:completeness}
+%
Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction. Si $\psi$ ne vérifie pas
la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible,
alors les itérations de $\phi$ ne sont pas universellement convergentes.
-\end{theorem}
+\end{restatable}
+
+
Le nombre de configurations est donc borné par $2^{m(\delta_0+1)+n(n+2)}$.
On remarque que cette borne est traitable par SPIN pour des valeurs raisonnables de $n$,
$m$ et $\delta_0$.
- \JFC{Donner un ordre de grandeur de cet ordre de grandeur}
+ %\JFC{Donner un ordre de grandeur de cet ordre de grandeur}
\end{Proof}
-La méthode détaillée ici a pu être appliquée sur l'exemple jouet
+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
l'automate de Büchi issu de cette formule et celui issu du programme PROMELA,
SPIN n'arrive pas à vérifier si la convergence universelle est établie
ou non sur des exemples
-simples\JFC{faire référence à un tel exemple}.
+simples.%\JFC{faire référence à un tel exemple}.
Ce problème a été pratiquement résolu en laissant SPIN
générer toutes les traces d'exécution,
La méthode détaillée ici a été appliquée sur des exemples pour prouver formellement
-leur convergence ou leur divergence (\Fig{fig:async:exp}).
+leur convergence ou leur divergence (\Fig{fig:exp:promela})
+avec ou sans délais.
Dans ces expériences, les délais ont été bornés par $\delta_0=10$.
Dans ce tableau, $P$ est vrai ($\top$) si et seulement si la convergence
universelle
pour établir un verdict.
-\begin{figure}
-\begin{center}
-\begin{tiny}
-\begin{tabular}{|*{7}{c|}}
-\cline{2-7}
-\multicolumn{1}{c|}{ }
-&\multicolumn{3}{|c|}{Parallèles} & \multicolumn{3}{|c|}{Chaotiques} \\
-\cline{2-7}
-\multicolumn{1}{c|}{ }&
-P & M & T&
-P & M & T \\
-\hline %\cline{2-7}
-\textit{RE} &
-$\top$ & 2.7 & 0.01s &
-$\bot$ & 369.371 & 0.509s \\
-\hline %\cline{2-7}
-\cite{RC07} &
-$\bot$ & 2.5 & 0.001s & % RC07_sync.spin
-$\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
-\hline
-\cite{BM99} &
-$\top$ & 36.7 & 12s & % BM99_sync_para.spin
-$\top$ & & \\ % BM99_sync_chao.spin
-\hline
-\end{tabular}
-\end{tiny}
-\end{center}
-\caption{Expérimentations avec des itérations synchrones}\label{fig:sync:exp}
-\end{figure}
-
-
-
-\begin{figure}
-\begin{center}
-\tiny
-\begin{tabular}{|*{13}{c|}}
-\cline{2-13}
-\multicolumn{1}{c|}{ }
-&\multicolumn{6}{|c|}{Mixed Mode} & \multicolumn{6}{|c|}{Only Bounded} \\
-\cline{2-13}
-\multicolumn{1}{c|}{ }
-&\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} &
-\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
-\cline{2-13}
-\multicolumn{1}{c|}{ }
-&P & M & T &
-P & M & T &
-P & M & T&
-P & M & T \\
-\hline %cline{2-13}
-\textit{RE} &
-$\top$ & 409 & 1m11s&
-$\bot$ & 370 & 0.54 &
-$\bot$ & 374 & 7.7s&
-$\bot$ & 370 & 0.51s \\
-\hline %\cline{2-13}
-AC2D
-&$\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
-&$\bot$ & 2.5 & 0.01s \\ % RC07_async_all.spin
-\hline %\cline{2-13}
-\cite{BM99}
-&$\top$ & & %BM99_mixed_para.spin
-&$\top$ & & % RC07_async_mixed_all.spin
-&$\bot$ & & % RC07_async.spin
-&$\bot$ & & \\ % RC07_async_all.spin
-\hline %\cline{2-13}
-\end{tabular}
-\end{center}
-\caption{Expérimentations avec des itérations asynchrones}\label{fig:async:exp}
+\begin{figure}[ht]
+ \begin{center}
+ \begin{tiny}
+ \subfigure[Sans délais]{
+ \begin{tabular}{|*{7}{c|}}
+ \cline{2-7}
+ \multicolumn{1}{c|}{ }
+ &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Généralisées} \\
+ \cline{2-7}
+ \multicolumn{1}{c|}{ }&
+ P & M & T&
+ P & M & T \\
+ \hline %\cline{2-7}
+ \textit{RE} &
+ $\top$ & 2.7 & 0.01s &
+ $\bot$ & 369.371 & 0.509s \\
+ \hline %\cline{2-7}
+ \cite{RC07} &
+ $\bot$ & 2.5 & 0.001s & % RC07_sync.spin
+ $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
+ \hline
+ \cite{BM99} &
+ $\top$ & 36.7 & 12s & % BM99_sync_para.spin
+ $\top$ & & \\ % BM99_sync_chao.spin
+ \hline
+ \end{tabular}
+ \label{fig:sync:exp}
+ }
+
+ \subfigure[Avec délais]{
+ \begin{tabular}{|*{13}{c|}}
+ \cline{2-13}
+ \multicolumn{1}{c|}{ }
+ &\multicolumn{6}{|c|}{Mode Mixe} & \multicolumn{6}{|c|}{Seulement borné} \\
+ \cline{2-13}
+ \multicolumn{1}{c|}{ }
+ &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Pseudo-Périodique} &
+ \multicolumn{3}{|c|} {Synchrones} & \multicolumn{3}{|c|}{Pseudo-Périodique} \\
+ \cline{2-13}
+ \multicolumn{1}{c|}{ }
+ &P & M & T &
+ P & M & T &
+ P & M & T&
+ P & M & T \\
+ \hline %cline{2-13}
+ \textit{RE} &
+ $\top$ & 409 & 1m11s&
+ $\bot$ & 370 & 0.54 &
+ $\bot$ & 374 & 7.7s&
+ $\bot$ & 370 & 0.51s \\
+ \hline %\cline{2-13}
+ AC2D
+ &$\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
+ &$\bot$ & 2.5 & 0.01s \\ % RC07_async_all.spin
+ \hline %\cline{2-13}
+ \cite{BM99}
+ &$\top$ & & %BM99_mixed_para.spin
+ &$\top$ & & % RC07_async_mixed_all.spin
+ &$\bot$ & & % RC07_async.spin
+ &$\bot$ & & \\ % RC07_async_all.spin
+ \hline %\cline{2-13}
+ \end{tabular}
+ \label{fig:async:exp}
+ }
+ \end{tiny}
+ \end{center}
+ \caption{Résultats des simulations Promela des SDDs}\label{fig:exp:promela}
\end{figure}
-L'exemple \textit{RE} est l'exemple jouet de ce chapitre,
+L'exemple \textit{RE} est l'exemple de ce chapitre,
\cite{RC07} concerne un réseau composé de deux gènes
à valeur dans $\{0,1,2\}$,
AC2D est un automate cellulaire avec 9 elements prenant des
valeurs booléennes en fonction de
de 4 voisins et
\cite{BM99} consiste en 10 process
-qui modifient leur valeur booléennes dans un graphe d'adjacence proche
+qui modifient leurs valeurs booléennes dans un graphe d'adjacence proche
du graphe complet.
-L'exemple jouet \textit{RE} a été prouvé comme universellement convergent.
+L'exemple \textit{RE} a été prouvé comme universellement convergent.
\JFC{statuer sur AC2D}
-Comme la convergence n'est déjà pas établie pour les itérations parallèles
+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.
La {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN de menant à la violation
\section{Conclusion}
\label{sec:spin:concl}
-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.
-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
-si et seulement si on peut construire une fonction de Lyaponov décroissante, mais il ne donne pas de méthode
-automatique pour construire cette fonction.
-\JFC{Déplacer ceci dans les perspective}
-Among drawbacks of the method, one can argue that bounded delays is only
-realistic in practice for close systems.
-However, in real large scale distributed systems where bandwidth is weak,
-this restriction is too strong. In that case, one should only consider that
-matrix $s^{t}$ follows the iterations of the system, \textit{i.e.},
-for all $i$, $j$, $1 \le i \le j \le n$, we have$
-\lim\limits_{t \to \infty} s_{ij}^t = + \infty$.
-One challenge of this work should consist in weakening this constraint.
-We plan as future work to take into account other automatic approaches
-to discharge proofs notably by deductive analysis~\cite{CGK05}.
