X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/103fee06d77ee199f8956ccb0747b45676c834e5..d33e664452e3655370cbe069e3f6fbd16842c818:/modelchecking.tex?ds=sidebyside diff --git a/modelchecking.tex b/modelchecking.tex index 1919416..96a8586 100644 --- a/modelchecking.tex +++ b/modelchecking.tex @@ -1,17 +1,15 @@ - - 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 @@ -19,20 +17,21 @@ si et seulement si on peut construire une fonction de Lyaponov décroissante, ma 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 repose alors que sur le verdict +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 vérifier automatiquement -qu'un modèle vérifie une propriété donnée. Pour traiter le problème d'explosion +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 selon toutes les sortes d'itérations 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 @@ -40,10 +39,10 @@ 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 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}. @@ -90,16 +89,17 @@ sont ensuite fournies (\Sec{sec:spin:practical}). -On peut facilement vérifier que toutes les itérations synchrones initialisées +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 mode unaires ou généralisés avec une +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é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} @@ -155,12 +155,12 @@ 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$; + ${\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 @@ -186,9 +186,9 @@ Dans l'exemple précédent, on déclare successivement: \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} @@ -210,8 +210,8 @@ réception de messages. Pour un canal 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 non rempli). -Dans les cas problématiques, canal non initialisé et vide pour une réception ou bien rempli pour un envoi, +\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 @@ -220,9 +220,9 @@ si plus d'une des conditions est établie, l'ensemble des instructions correspon 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 $N$ initialise aléatoirement la variable globale de type tableau \verb+Xp+. +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)}$. +quelle configuration initiale $x^{0}$. @@ -345,7 +345,7 @@ 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 à $n$ choix successifs) et sont mémorisés dans le tableau +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 @@ -432,7 +432,7 @@ inline F(){ \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)}) @@ -458,8 +458,8 @@ dans la section suivante; 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} @@ -537,7 +537,7 @@ 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 +\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é ( @@ -590,7 +590,7 @@ délai. \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 à $n$ éléments est universellement convergent. +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. @@ -602,7 +602,7 @@ de prouver la formule temporelle linéaire (LTL) suivante: \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 @@ -652,12 +652,12 @@ 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 à $n$ éléments, $m$ + 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é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. @@ -669,18 +669,18 @@ puis présente ensuite les expérimentations issues de ce travail. 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 $n$, + 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} +\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$: @@ -764,7 +764,7 @@ pour établir un verdict. \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} & @@ -782,7 +782,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 @@ -806,36 +806,30 @@ pour établir un verdict. 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 +à 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} +%\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 de menant à la violation +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. - -\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 +862,18 @@ 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 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.