la veille

[hdrcouchot.git] / modelchecking.tex

Sur des petits exemples, 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és, le problème 
se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones 
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 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 
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 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 
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 adressent le problème de détecter automatiquement
si 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  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érimentations
sont ensuite fournies (\Sec{sec:spin:practical}). 
Ce chapitre a fait l'objet du rapport~\cite{Cou10:ir}.






%\section{Exemple jouet}


\begin{figure}[ht]
  \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  \\
          f_2(x_1,x_2,x_3) & = & x_1 + \overline{x_3} \\
          f_3(x_1,x_2,x_3) & = & x_2.x_3
        \end{array}
      \right.
      $        
      \label{fig:map}
    }
    \hfill
    \subfigure[Graphe d'intéraction]{
      \includegraphics[width=4cm]{images/xplCnxMc.eps}
      \label{fig:xplgraph:inter:mc}
    }
  \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 élément 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:inter:mc} donne son graphe d'intéraction.
  






On peut facilement vérifier que toutes les itérations parallèles 
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  modes 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é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}   
\end{xpl}





\section{Rappels sur le langage PROMELA}
\label{sec:spin:promela}

Cette section  rappelle les éléments fondamentaux du langage PROMELA (Process Meta  Language).
On peut trouver davantage de détails dans~\cite{Hol03,Wei97}.




\begin{figure}[ht]
\begin{tiny}
\begin{lstlisting}
#define N 3
#define d_0 5

bool X [N]; bool Xp [N]; int mods [N];
typedef vals{bool v [N]};
vals Xd [N];  

typedef a_send{chan sent[N]=[d_0] of {bool}};
a_send channels [N];

chan unlock_elements_update=[1] of {bool};
chan sync_mutex=[1] of {bool};
\end{lstlisting}
\end{tiny}
\caption{Declaration des types de la traduction.}
\label{fig:arrayofchannels}
\end{figure}


% 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.

\begin{xpl}
Le programme donné à la {\sc Figure}~\ref{fig:arrayofchannels} correspond à des 
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
 ${\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$ 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 
 \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}$).
\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.

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  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
 \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 éléments $i$.
\item les deux canaux  \verb+unlock_elements_update+ et  \verb+sync_mutex+ contenant 
chacun un message booléen et sont utilisés ensuite comme des sémaphores.
\end{itemize}
\end{xpl}

%\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  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 
d'initialiser les variables, lancer d'autres process\ldots


Les instructions d'affectation sont interprétées usuellement.
Les canaux sont concernés par des instructions particulières d'envoi et de
réception de messages. Pour un canal  
\verb+ch+,  ces instructions sont respectivement notées
\verb+ch ! m+ et \verb+ch ? m+.
L'instruction de réception consomme la valeur en tête du canal \verb+ch+
et l'affecte à la variable \verb+m+ (pour peu que  \verb+ch+ soit initialisé et non vide).
De manière similaire, l'instruction d'envoi ajoute la valeur de \verb+m+ à la queue du canal
\verb+ch+ (pour peu que celui-ci soit initialisé et pas plein).
Dans les cas problématiques, canal non initialisé et vide pour une réception ou plein pour un envoi,
le processus est bloqué jusqu'à ce que les  conditions soient  remplies.

La structures de contrôle   \verb+if+   (resp.   \verb+do+)   définit un choix non déterministe 
 (resp.  une boucle non déterministe). Que ce soit pour la conditionnelle ou la boucle, 
si plus d'une des conditions est établie, l'ensemble des instructions correspondantes 
sera choisi aléatoirement puis exécuté.

Dans le process \verb+init+ détaillé à la {\sc Figure}~\ref{fig:spin:init}, 
une boucle de taille ${\mathsf{N}}$ initialise aléatoirement la variable  globale de type tableau \verb+Xp+.
Ceci permet par la suite de vérifier si les itérations sont  convergentes pour n'importe  
quelle configuration initiale $x^{0}$.



Pour chaque  élément $i$, si les itérations sont asynchrones
\begin{itemize}
\item on stocke d'abord la valeur de \verb+Xp[i]+ dans chaque \verb+Xd[j].v[i]+ 
puisque la matrice $s^0$ est égale à $(0)$,
\item puis, la valeur  de $i$ (représentée par  \verb+Xp[i]+) devrait être transmise 
  à $j$  s'il y a un arc de $i$ à   $j$ dans le graphe d'incidence. Dans ce cas,
  c'est la fonction  \verb+hasnext+ (détaillée à la~\Fig{fig:spin:hasnext})  
  qui   mémorise ce graphe
  en fixant à  \texttt{true} la variable \verb+is_succ+, naturellement et à 
  \texttt{false} dans le cas contraire. 
  Cela permet d'envoyer la valeur de $i$ dans le canal au travers de \verb+channels[i].sent[j]+.
\end{itemize}

\begin{figure}[t]
  \begin{minipage}[h]{.32\linewidth}
\begin{tiny}
\begin{lstlisting}
init{
 int i=0; int j=0; bool is_succ=0;
 do
 ::i==N->break;
 ::i< N->{
   if
   ::Xp[i]=0;
   ::Xp[i]=1;
   fi;
   j=0;
   do
   ::j==N -> break;
   ::j< N -> Xd[j].v[i]=Xp[i]; j++;
   od;
   j=0;
   do
   ::j==N -> break;
   ::j< N -> {
     hasnext(i,j);
     if
     ::(i!=j && is_succ==1) -> 
     channels[i].sent[j] ! Xp[i];
     ::(i==j || is_succ==0) -> skip; 
     fi;  
     j++;}
   od;
   i++;}
 od;
 sync_mutex ! 1;
}
\end{lstlisting}
\end{tiny}
\caption{Process init.}\label{fig:spin:init} 
\end{minipage}\hfill
 \begin{minipage}[h]{.32\linewidth}
\begin{tiny}
\begin{lstlisting}
active proctype scheduler(){ 
 do
 ::sync_mutex ? 1 -> {
   int i=0; int j=0;
   do
   :: i==N -> break;
   :: i< N -> {
     if
     ::skip;
     ::mods[j]=i; j++;
     fi;
     i++;}
   od;
   ar_len=i; 
   unlock_elements_update ! 1;
   }
 od
}
\end{lstlisting}
\end{tiny}
\caption{Process scheduler pour la stratégie pseudo-périodique.
 \label{fig:scheduler}}
\end{minipage}
\begin{minipage}[h]{.30\linewidth}
\begin{tiny}
\begin{lstlisting}
inline hasnext(i,j){
  if
    :: i==0 && j ==0 -> is_succ = 1
    :: i==0 && j ==1 -> is_succ = 1
    :: i==0 && j ==2 -> is_succ = 0
    :: i==1 && j ==0 -> is_succ = 1
    :: i==1 && j ==1 -> is_succ = 0
    :: i==1 && j ==2 -> is_succ = 1
    :: i==2 && j ==0 -> is_succ = 1     
    :: i==2 && j ==1 -> is_succ = 1
    :: i==2 && j ==2 -> is_succ = 1
  fi
}
\end{lstlisting}
\end{tiny}
\caption{Codage du graphe d'intéraction de $f$.
 \label{fig:spin:hasnext}}
\end{minipage}

\end{figure}



\section{Du système booléen au modèle PROMELA}
\label{sec:spin:translation}
Les éléments principaux des itérations asynchrones rappelées à l'équation 
(\ref{eq:async}) sont  la stratégie, la  fonctions et la gestion des délais.
Dans cette section, nous présentons successivement comment chacune de 
ces notions est traduite vers un modèle PROMELA.


\subsection{La stratégie}\label{sub:spin:strat}
Regardons comment une stratégie pseudo-périodique peut être représentée en PROMELA.
Intuitivement, un process \verb+scheduler+ (comme représenté à la {\sc Figure}~\ref{fig:scheduler}) 
est itérativement appelé pour construire chaque $s^t$ représentant 
les éléments possiblement mis à jour à l'itération $t$.

Basiquement, le process est une boucle qui est débloquée lorsque la valeur du sémaphore
\verb+sync_mutex+ est 1. Dans ce cas, les éléments à modifier sont choisis
aléatoirement  (grâce à  ${\mathsf{N}}$ choix successifs) et sont mémorisés dans le tableau
\verb+mods+,  dont la taille est  \verb+ar_len+.   
Dans la séquence d'exécution, le choix d'un élément mis à jour est directement
suivi par des mises à jour: ceci est réalisé grâce à la modification de la valeur du sémaphore
 \verb+unlock_elements_updates+.

\subsection{Itérer la fonction $f$}\label{sub:spin:update}
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 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:

\begin{figure}[t]
\begin{minipage}[b]{.32\linewidth}
\begin{tiny}
\begin{lstlisting}
inline update_X(){      
  int countu;
  countu = 0;
  do
    :: countu == N -> break ;
    :: countu != N ->
       X[countu] = Xp[countu];
       countu ++ ;
  od
}
\end{lstlisting}
\end{tiny}
\caption{Sauvegarde de l'état courant}\label{fig:spin:sauve}
\end{minipage}\hfill%
\begin{minipage}[b]{.32\linewidth}
\begin{tiny}
\begin{lstlisting}
active proctype update_elems(){
 do
 ::unlock_elements_update ? 1 ->
   {
    atomic{
     bool is_succ=0;
     update_X();
     fetch_values();
     int count = 0;
     int j = 0;
     do
     ::count == ar_len -> break;
     ::count < ar_len ->
       j = mods[count];     
       F(j);
       count++;
     od;
     diffuse_values(Xp);
     sync_mutex ! 1
    }
   }
 od
}
\end{lstlisting}
\end{tiny}
\caption{Mise à jour des éléments}\label{fig:proc}
  \end{minipage}\hfill%
%\end{figure}
%\begin{figure}
  \begin{minipage}[b]{.33\linewidth}
\begin{tiny}
\begin{lstlisting}
inline F(){
 if
 ::j==0 -> Xp[0] = 
      (Xs[j].v[0] & !Xs[j].v[1]) 
     |(Xs[j].v[2])
 ::j==1 -> Xp[1] =  Xs[j].v[0] 
                 | !Xs[j].v[2]
 ::j==2 -> Xp[2] =  Xs[j].v[1] 
                 &  Xs[j].v[2]
 fi
}
\end{lstlisting}
\end{tiny}
\caption{Application de la fonction $f$}\label{fig:p}
  \end{minipage}
\end{figure}


\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 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)})
  pour peu que celui-ci doive être modifié,  \textit{i.e.},   pour peu qu'il soit renseigné dans
  \texttt{mods[count]}; le code source de \texttt{F} est donné en {\sc Figure}~\ref{fig:p} et est une 
  traduction directe de l'application $f$;
\item les nouvelles valeurs des éléments \texttt{Xp} sont symboliquement
  envoyés aux autres éléments qui en dépendent grâce à la fonction 
  \texttt{diffuse\_values(Xp)}; cette dernière fonction est aussi détaillée 
  dans la section suivante; 
\item finalement, le process informe le scheduler de la fin de la tâche 
  (au travers  du sémaphore \texttt{sync\_mutex}).
\end{enumerate}








\subsection{Gestion des délais}\label{sub:spin:vt}
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}. 
Elles récupèrent et diffusent respectivement les valeurs des éléments.

\begin{figure}[t]
  \begin{minipage}[h]{.475\linewidth}
\begin{tiny}
\begin{lstlisting}
inline fetch_values(){
 int countv = 0;
 do
 :: countv == ar_len -> break ;
 :: countv < ar_len ->
    j = mods[countv];
    i = 0;       
    do
    :: (i == N) -> break;
    :: (i < N && i == j) -> {
        Xd[j].v[i] = Xp[i] ;
        i++ }   
    :: (i < N && i != j) -> {
        hasnext(i,j);
        if
        :: skip
        :: is_succ==1 &&
    nempty(channels[i].sent[j]) ->
            channels[i].sent[j] ?
                        Xd[j].v[i];
        fi; 
        i++ }
    od;
    countv++
 od
}
\end{lstlisting}
\end{tiny}
\caption{Récupérer les valeurs des elements\label{fig:val}}
  \end{minipage}\hfill%
  \begin{minipage}[h]{.475\linewidth}
\begin{tiny}
\begin{lstlisting}
inline diffuse_values(values){   
 int countb=0;
 do
 :: countb == ar_len -> break ;
 :: countb < ar_len ->
    j = mods[countb];
    i = 0 ;
    do
    :: (i == N) -> break;
    :: (i < N && i == j) -> i++;   
    :: (i < N && i != j) -> {
        hasnext(j,i);
        if
        :: skip
        :: is_succ==1 && 
     nfull(channels[j].sent[i]) ->
            channels[j].sent[i] ! 
                         values[j];
        fi;
        i++ }
    od;
    countb++
 od
}       
\end{lstlisting}
\end{tiny}
\caption{Diffuser les valeurs des elements}\label{fig:broadcast}
  \end{minipage}
\end{figure}

La première fonction met à jour le tableau   \verb+Xd+ requis pour les éléments
qui doivent être modifiés.
Pour chaque élément dans  \verb+mods+, identifié par la variable 
$j$, la fonction récupère les valeurs  des autres éléments  (dont le libellé est $i$)
dont $j$ dépend. 
Il y a deux cas.
\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 
  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é  (c'est l'instruction \verb+skip+) ou n'est pas utile; ce dernier cas apparaît 
    lorsqu'il n'y a pas d'arc de  $i$ à $j$ dans le graphe d'incidence, \textit{i.e.}, lorsque
    la valeur de \verb+is_succ+ qui est calculée par  \verb+hasnext(i,j)+ est 0;
    dans ce cas, la valeur de \verb+Xd[j].v[i]+ n'est pas modifiée;
  \item sinon,  on affecte à \verb+Xd[j].v[i]+ la valeur mémorisée
    dans le canal \verb+channels[i].sent[j]+  (pour peu que celui-ci ne soit pas vide).
  \end{itemize}
\end{itemize}

Les valeurs des éléments sont ajoutées dans ce canal au travers de la fonction  \verb+diffuse_values+. L'objectif de cette fonction 
est de stocker les valeurs de $x$  (représenté
dans le modèle par \verb+Xp+) dans le canal  \verb+channels+.
Il permet au model-checker SPIN  d'exécuter 
le modèle PROMELA   comme s'il pouvait y avoir des délais entre processus.
Il y a deux cas différents pour la valeur de $X_{j}$:
\begin{itemize}
\item soit elle est \og perdue\fg{}, \og oubliée\fg{} pour permettre à $i$ de ne pas tenir compte d'une 
des valeurs de  $j$; ce cas a lieu soit lors de l'instruction  \verb+skip+ ou lorsqu'il 
n'y a pas d'arc de $j$ à $i$ dans le graphe d'incidence;
\item soit elle est mémorisée dans le canal \verb+channels[j].sent[i]+ (pour peu que celui-ci ne soit pas plein).
\end{itemize}

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 
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 
mise dans le canal, elle serait immédiatement consommée, ce qui est contradictoire avec la notion de 
délai.

% \subsection{Discussion}
% A  coarse approach  could consist  in providing  one process  for  each element.
% However, the  distance with  the mathematical model  given in  \Equ{eq:async} of
% such a translation would be larger  than the method presented along these lines.
% It induces  that it would be harder  to prove the soundness  and completeness of
% such a translation.   For that reason we have developed a  PROMELA model that is
% as close as possible to the mathematical one.

% Notice furthermore that PROMELA is an  imperative language which
% often results in generating  intermediate  states 
% (to  execute  a matrix assignment  for
% instance). 
% The  use  of  the  \verb+atomic+  keyword  allows  the  grouping  of
% instructions, making the PROMELA code and the DDN as closed as possible.

\subsection{Propriété de convergence universelle}
Il reste à formaliser dans le model checker SPIN le fait que les 
itérations d'un système 
dynamique à ${\mathsf{N}}$ éléments est universellement convergent.

Rappelons tout d'abord que les variables \verb+X+  et \verb+Xp+ 
contiennent respectivement la valeur de $x$ avant et après la mise à jour. 
Ainsi, si l'on effectue une initialisation  non déterministe de 
\verb+Xp+  et si l'on applique une stratégie pseudo-périodique,  
il est nécessaire et suffisant
de prouver la formule temporelle linéaire (LTL) suivante:
\begin{equation}
\diamond  (\Box  \verb+Xp+ = \verb+X+)
\label{eq:ltl:conv}
\end{equation}
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
la stabilisation du système.
Cependant elle ne donne aucune métrique quant à
la manière dont celle-ci est obtenue.
En particulier, on peut converger très lentement ou le système peut même 
disposer de plusieurs points fixes.



\section{Correction et complétude de la démarche}\label{sec:spin:proof}

Cette section présente les théorèmes
de correction et de  complétude de l'approche
(Théorèmes~\ref{Theo:sound} et~\ref{Theo:completeness}). 
Toutes les preuves sont déplacées en 
annexe~\ref{anx:promela}.


\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{restatable}


\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{restatable}






\section{Données pratiques}
\label{sec:spin:practical}
Cette section donne tout d'abord quelques mesures de complexité de l'approche 
puis présente ensuite les expérimentations issues de ce travail.

\begin{theorem}[Nombre d'états]
  Soit  $\phi$  un modèle de système dynamique discret à  ${\mathsf{N}}$ éléments, $m$ 
  arcs dans le graphe d'incidence
  et $\psi$ sa traduction en PROMELA.  Le nombre de configurations 
  de l'exécution en SPIN de $\psi$ est borné par $2^{m(\delta_0+1)+n(n+2)}$.
\end{theorem}
\begin{proof}
  Une configuration est une évaluation des variables globales.
  Leur nombre ne dépend que de celles qui ne sont pas constantes.

  Les  variables  \verb+Xp+ et \verb+X+ engendrent  $2^{2n}$ états.
  La variable
  \verb+Xs+ génère $2^{n^2}$ états.  
  Chaque canal de \verb+array_of_channels+
  peut engendrer $1+2^1+\ldots+2^{\delta_0}=  2^{\delta_0+1}-1$  états. 
  Puisque le nombre d'arêtes du graphe d'incidence  est $m$,  
  il y a  $m$ canaux non constants,  ce qui génère approximativement $2^{m(\delta_0+1)}$ états. 
  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  ${\mathsf{N}}$, 
  $m$ et $\delta_0$.
  %\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
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édents reposent sur le fait que 
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$:  
$$
\Box \diamond (l == l_0) \Rightarrow 
((\Box \diamond (l== l_1)) \land  \ldots \land (\Box \diamond (l == l_k)))
$$

où le libellé $l_0$ dénote le libellé de la ligne précédent 
le choix indéterministe.
Cette formule traduit exactement l'équité faible.
Cependant en raison de l'explosion de la taille du produit entre 
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}. 

Ce problème a été pratiquement résolu en laissant SPIN 
générer toutes les traces d'exécution,
même celles qui ne sont pas équitables, 
puis ensuite vérifier la propriété de convergence sur toutes celles-ci. 
Il reste alors à interpréter les résultats qui peuvent être de deux types. Si la convergence est 
établie pour toutes les traces, elle le reste en particulier pour les traces équitables.
Dans le cas contraire on doit analyser le contre exemple produit par SPIN.

% \begin{xpl}
% \JFC{Reprendre ce qui suit}
% Experiments have shown that all the iterations of the running example are 
% convergent for a delay equal to 1 in less than 10 min.
% The example presented in~\cite{abcvs05} with five elements taking boolean 
% values has been verified with method presented in this article.   
% Immediately, SPIN computes a counter example, that unfortunately does not
% fulfill fairness properties. Fair counter example is obtained
% after few minutes.
% All the experimentation have been realized in a classic desktop computer.
% \end{xpl}


La méthode détaillée ici a été appliquée sur des exemples pour prouver formellement 
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 
est établie et faux ($\bot$) sinon. Le nombre $M$ est 
la taille de la  mémoire consommée (en MB) et 
$T$ est le temps d'exécution sur un  Intel Centrino Dual Core 2 Duo @1.8GHz avec 2GB de mémoire vive
pour établir un verdict.


\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 Mixte} & \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}
          \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
          &$\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 de ce chapitre,
\cite{RC07} concerne un réseau composé de deux gènes
à valeur dans $\{0,1,2\}$ et
\cite{BM99} consiste en  10 process
qui modifient leurs valeurs booléennes dans un graphe d'adjacence proche 
du graphe complet.


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 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  menant à la violation 
de la convergence. Celle-ci correspond à une stratégie périodique qui répète
$\{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, montrant les limites de
l'approche.

\begin{figure}
\centering
\includegraphics[scale=0.6]{images/RC07ce.eps}   
\caption{Contre exemple de convergence pour~~\cite{RC07}} \label{fig:RC07CE}
\end{figure}







% \begin{tabular}{|*{19}{c|}}
% % \hline 
% % e \\
% % 
% \hline
% & \multicolumn{6}{|c|}{Synchronous} & \multicolumn{12}{|c|}{Asynchronous}\\
% \cline{8-19}
% Delay &  \multicolumn{6}{|c|}{ }
% & \multicolumn{6}{|c|}
% {Only Bounded}
% & \multicolumn{6}{|c|}
% {Bounded+Mixed Mode}\\
% Strategy&
% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} &
% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} &
% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} \\


%  \end{tabular}

 
\section{Conclusion}
\label{sec:spin:concl}

L'idée principale de ce chapitre est que l'on peut, 
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 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 
convergent pas.