From 9e9f22c16917d3bf287f5e1f0df739200c392594 Mon Sep 17 00:00:00 2001 From: couchot Date: Wed, 31 Aug 2016 08:46:41 +0200 Subject: [PATCH] preuve promela:debut de traduction --- ahmad.tex | 12 ++- annexePreuveMixage.tex | 14 ++- annexePromelaProof.tex | 149 +++++++++++++++++--------------- demandeInscription/synthese.tex | 5 +- main.tex | 8 +- mixage.tex | 13 ++- modelchecking.tex | 43 +++++---- sdd.tex | 29 +++---- stabylo.tex | 2 +- stegoyousra.tex | 34 +++----- 10 files changed, 153 insertions(+), 156 deletions(-) diff --git a/ahmad.tex b/ahmad.tex index 1b92dbc..05d9177 100644 --- a/ahmad.tex +++ b/ahmad.tex @@ -20,7 +20,13 @@ préétablies et conserver ainsi leur information et donc la marque. STDM~\cite{CW01} est une instance de ces schémas de marquage. Ce chapitre présente une application de STDM au marquage de documents PDFs. -\JFC{annonce du plan} +La première section fournit quelques rappels sur la STDM. Le schéma basé sur +cette approche est présenté à la section~\ref{sec:stdm:schema}. +Finalement, la démarche expérimentale permettant de trouver un compromis entre +robustesse et qualité visuelle est présentée à la section~\ref{sec:stdm:exp} +Ce travail a été publié dans~\cite{BDCC16}. + + \section{Rappels sur la Spread Transform Dither Modulation} \label{sec:STDM} @@ -66,7 +72,7 @@ $U(\Delta)$. Tous les éléments sont en place pour embarquer une marque dans un fichier PDF selon le schéma STDM. -\section{Application au marquage de documents PDF} +\section{Application au marquage de documents PDF}\label{sec:stdm:schema} On détaille successivement comment insérer une marque dans un document PDF, puis comment l'extraire. @@ -132,7 +138,7 @@ de taille $L$ mutuellement disjoints dans $[1,N]$. en remplaçant $x'$ par $\dot{x'}$ . \end{enumerate} -\section{Expérimentations } +\section{Expérimentations}\label{sec:stdm:exp} Le schéma de marquage est paramétré par $\Delta$, $d_0$ et la manière de construire le vecteur $p$ pour une taille $L$. Les travaux réalisés se sont focalisés sur l'influence du paramètre $D_S = \frac{\Delta^2}{12L}$ dans l'algorithme en satisfaisant diff --git a/annexePreuveMixage.tex b/annexePreuveMixage.tex index d4087d4..12c3223 100644 --- a/annexePreuveMixage.tex +++ b/annexePreuveMixage.tex @@ -3,11 +3,9 @@ $\preceq$ entre les classes d'équivalences. Formellement, \class{p} $\preceq$ \class{q} s'il existe un chemin de longueur $\alpha$ -($0<\alpha<|\mathcal{K}|$) entre un élément le la classe +($0\le\alpha<|\mathcal{K}|$) entre un élément le la classe \class{p} vers un élément de -\class{q}. -On remarque que si la \class{p}$\preceq$\class{q}, -il n'est alors pas possible que \class{q}$\preceq$\class{p}. +\class{q}. \begin{lemma} Il existe un processus de renommage qui effecte un nouvel identifiant aux @@ -17,7 +15,7 @@ il n'est alors pas possible que \class{q}$\preceq$\class{p}. \begin{Proof} Tout d'abord, soit \class{p_1}, \ldots, \class{p_l} des classes - contenant respectivement $n_1$,\ldots, $n_l$ éléments respectively + contenant respectivement les éléments $n_1$,\ldots, $n_l$ qui ne dépendent d'aucune autre classe. Les éléments de \class{p_1} sont renommés par $1$, \ldots, $n_1$, les elements de \class{p_i}, $2 \le i \le l$ sont renommés par @@ -72,7 +70,7 @@ On peut remarquer que ce processus de renommage est inspiré des \emph{graphes % Processes numbers are already compliant with the order $\preceq$. % \end{xpl} -\begin{Proof}[of Theorem~\ref{th:cvg}] +\begin{Proof}[du théorème~\ref{th:cvg}] Le reste de la preuve est fait par induction sur le numéro de classe. Considérons la première classe \class{b_1} de $n_1$ éléments @@ -95,10 +93,10 @@ On peut remarquer que ce processus de renommage est inspiré des \emph{graphes pour chaque $p_{k+1} \in$ \class{b_{k+1}} et $p_j \in$ \class{b_j}, $1 \le j \le k$. - Il nous reste donc des itérations synchronous entre les + Il ne reste donc que des itérations synchrones entre les elements of \class{b_{k+1}} en démarant dans des configurations où tous les éléments de \class{b_j}, $1 \le j - \le k$, on des valeurs constantes. + \le k$, ont des valeurs constantes. D'après les hypothèses du théorème, cela converge. \end{Proof} diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex index 70981a9..881383c 100644 --- a/annexePromelaProof.tex +++ b/annexePromelaProof.tex @@ -1,10 +1,10 @@ -\JFC{Voir section~\ref{sec:spin:proof}} +%\JFC{Voir section~\ref{sec:spin:proof}} Cette section donne les preuves des deux théorèmes de correction et complétude du chapitre~\ref{chap:promela}. -\begin{lemma}[Strategy Equivalence]\label{lemma:strategy} +\begin{lemma}[Stratégie équivalente]\label{lemma:strategy} Soit $\phi$ un système dynamique discret de stratégie $(S^t)^{t \in \Nats}$ et $\psi$ sa traduction en promela. Il existe une exécution de $\psi$ sous hypothèse d'équité faible telle @@ -20,7 +20,7 @@ du chapitre~\ref{chap:promela}. \end{Proof} Dans ce qui suit, soit $Xd^t_{ji}$ la valeur de -\verb+Xd[+$j$\verb+].v[+$i$\verb+]+ après le $t^{\text{th}}$ appel +\verb+Xd[+$j$\verb+].v[+$i$\verb+]+ après le $t^{\text{ème}}$ appel à la fonction \verb+fetch_values+. De plus, soit $Y^k_{ij}$ l'élément à l'indice $k$ @@ -62,11 +62,11 @@ permet de modéliser l'équation \Equ{eq:async}. La function $M_{ij}^{t+1}$ est obtenue à l'aide de mises à jour successives de $M_{ij}^{t}$ au travers des deux functions \verb+fetch_values+ and \verb+diffuse_values+. Par abus, soit $M_{ij}^{t+1/2}$ -la valeur de $M_{ij}^{t}$ après la première fonctions pendant l'itération +la valeur de $M_{ij}^{t}$ après la première fonction pendant l'itération $t$. Dans ce qui suit, on considère les éléments $i$ et $j$ -dans $\llbracket n \rrbracket$. +dans $[ \mathsf{N} ]$. A l'itération $t$, $t \geq 1$, soit $(Y^0_{ij},a^0_{ij},c^0_{ij})$ la valeur de $M_{ij}^t(0)$ en entrant dans la fonction @@ -97,7 +97,7 @@ est exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$. Pour chaque sequence $(S^t)^{t \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$, pour chaque fonction $F$, il existe une exécution SPIN telle que pour toute itération $t$, $t - \ge 1$, et pour chaque $i$ et $j$ in $\llbracket n \rrbracket$ + \ge 1$, et pour chaque $i$ et $j$ dans $[ \mathsf{N} ]$ on a la propriété suivante: \noindent Si le domaine de $M_{ij}^t$ n'est pas vide, alors @@ -105,7 +105,7 @@ est exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$. \left\{ \begin{array}{rcl} M_{ij}^1(0) & = & \left(X_i^{D_{ji}^{0}}, 0,0 \right) \\ - \textrm{sit $t \geq 2$ alors }M_{ij}^t(0) & = & + \textrm{si $t \geq 2$ alors }M_{ij}^t(0) & = & \left(X_i^{D_{ji}^{c}},D_{ji}^{c},c \right) \textrm{, } c = \min\{l | D_{ji}^l > D_{ji}^{t-2} \} \end{array} @@ -117,11 +117,11 @@ est exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$. \forall t'\, .\, 1 \le t' \le t \Rightarrow Xd^{t'}_{ji} = X^{D^{t'-1}_{ji}}_i \label{eq:correct_retrieve} \end{equation} -\noindent Enfin, pour chaque $k\in S^t$, la valeurde +\noindent Enfin, pour chaque $k\in S^t$, la valeur de la variable \verb+Xp[k]+ en sortant du processus \verb+update_elems+ est égale à $X_k^{t}$ \textit{i.e.}, $F_{k}\left( X_1^{D_{k\,1}^{t-1}},\ldots, - X_{n}^{D_{k\,{n}}^{t-1}}\right)$ à la fin de la $t^{\text{th}}$ itération. + X_{\mathsf{N}}^{D_{k\,{\mathsf{N}}}^{t-1}}\right)$ à la fin de la $t^{\text{th}}$ itération. \end{lemma} \begin{Proof} La preuve est faite par induction sur le nombre d'itérations. @@ -130,20 +130,20 @@ La preuve est faite par induction sur le nombre d'itérations. Pour le premier item, par definition de $M_{ij}^t$, on a $M_{ij}^1(0) = \left( \verb+Xp[i]+, 0,0 \right)$ qui est égal à $\left(X_i^{D_{ji}^{0}}, 0,0 \right)$. -Ensuite, lepremier appel à la fonction \verb+fetch_value+ +Ensuite, le premier appel à la fonction \verb+fetch_value+ soit affecte à la tête de \verb+channels[i].sent[j]+ à \verb+Xd[j].v[i]+ soit ne modifie par \verb+Xd[j].v[i]+. Grâce au processus \verb+init+ process, les deux cas sont égaux à \verb+Xp[i]+, \textit{i.e.}, $X_i^0$. L'equation (\ref{eq:correct_retrieve}) est ainsi établie. -Pour le dernier item, soit $k$, $0 \le k \le n-1$. +Pour le dernier item, soit $k$, $0 \le k \le \mathsf{N}-1$. A la fin de la première exécution du processus \verb+update_elems+, -la valur de +la valeur de \verb+Xp[k]+ est $F(\verb+Xd[+k\verb+].v[0]+, \ldots, -\verb+Xd[+k\verb+].v[+n-1\verb+]+)$. +\verb+Xd[+k\verb+].v[+\mathsf{N}-1\verb+]+)$. Ainsi par définition de $Xd$, ceci est égal à -$F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$. Grâce à l'équation \Equ{eq:correct_retrieve}, +$F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,\mathsf{N}-1})$. Grâce à l'équation \Equ{eq:correct_retrieve}, on peut conclure la preuve. @@ -157,79 +157,84 @@ n'est pas vide, par hypothèse d'induction $M_{ij}^{l}(0)$ est $\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c \right)$ où $c$ est $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$. -A l'itération $l$, si $l < c + 1$ alors \verb+skip+ statement is executed in -the \verb+fetch_values+ function. Thus, $M_{ij}^{l+1}(0)$ is equal to -$M_{ij}^{l}(0)$. Since $c > l-1$ then $D_{ji}^c > D_{ji}^{l-1}$ and hence, $c$ -is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Obviously, this implies also that -$D_{ji}^c > D_{ji}^{l-2}$ and $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$. - -We now consider that at iteration $l$, $l$ is $c + 1$. In other words, $M_{ij}$ -is modified depending on the domain $\dom(M^l_{ij})$ of $M^l_{ij}$: +A l'itération $l$, si $l < c + 1$ alors l'instruction + \verb+skip+ est exécutée dans la fonction \verb+fetch_values+. + Ainsi, $M_{ij}^{l+1}(0)$ est égal à +$M_{ij}^{l}(0)$. Puisque $c > l-1$, alors $D_{ji}^c > D_{ji}^{l-1}$ et donc, $c$ +est $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. +Cela implique que +$D_{ji}^c > D_{ji}^{l-2}$ et $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$. + +On considère maintenant qu'à l'itération $l$, celui-ci vaut $c + 1$. +Dit autrement, $M_{ij}$ est modifié en fonction du domaine $\dom(M^l_{ij})$ de + $M^l_{ij}$: \begin{itemize} -\item if $\dom(M_{ij}^{l})=\{0\}$ and $\forall k\, . \, k\ge l \Rightarrow - D^{k}_{ji} \neq l$ is established then $\dom(M_{ij}^{l+1})$ is empty and the - first item of the lemma is established; -\item if $\dom(M_{ij}^{l})=\{0\}$ and $\exists k\, . \, k\ge l \land D^{k}_{ji} - = l$ is established then $M_{ij}^{l+1}(0)$ is $(\verb+Xp[i]+,l,c_{ij})$ that - is added in the \verb+diffuse_values+ function s.t.\linebreak $c_{ij} = - \min\{k \mid D^{k}_{ji} = l \} $. Let us prove that we can express - $M_{ij}^{l+1}(0)$ as $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$ where - $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. First, it is not hard to - establish that $D_{ji}^{c_{ij}}= l \geq D_{ji}^{l} > D_{ji}^{l-1}$ and thus - $c_{ij} \geq c'$. Next, since $\dom(M_{ij}^{l})=\{0\}$, then between - iterations $D_{ji}^{c}+1$ and $l-1$, the \texttt{diffuse\_values} function has - not updated $M_{ij}$. Formally we have +\item si $\dom(M_{ij}^{l})=\{0\}$ et $\forall k\, . \, k\ge l \Rightarrow + D^{k}_{ji} \neq l$ sont vraies, alors $\dom(M_{ij}^{l+1})$ est vide et le premier + item du lemme est vérifié; +\item si $\dom(M_{ij}^{l})=\{0\}$ et $\exists k\, . \, k\ge l \land D^{k}_{ji} + = l$ sont vraies, alors $M_{ij}^{l+1}(0)$ vaut $(\verb+Xp[i]+,l,c_{ij})$ qui est ajouté + dans la fonction \verb+diffuse_values+ de sorte que $c_{ij} = + \min\{k \mid D^{k}_{ji} = l \} $. + Prouvons qu'on peut exprimer + $M_{ij}^{l+1}(0)$ comme $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$ où + $c'$ vaut $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. + Tout d'abord, il n'est pas difficile de prouver que + $D_{ji}^{c_{ij}}= l \geq D_{ji}^{l} > D_{ji}^{l-1}$ et que + $c_{ij} \geq c'$. + Ensuite, comme $\dom(M_{ij}^{l})=\{0\}$, alors, entre les + itérations $D_{ji}^{c}+1$ et $l-1$, la fonction \texttt{diffuse\_values} n'a pas mis à jour + $M_{ij}$. On a ainsi la propriété $$ \forall t,k \, .\, D_{ji}^c < t < l \land k \geq t \Rightarrow D_{ji}^k \neq t.$$ -Particularly, $D_{ji}^{c'} \not \in \{D_{ji}^{c}+1,\ldots,l-1\}$. We can apply -the third item of the induction hypothesis to deduce -$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ and we can conclude. - -\item if $\{0,1\} \subseteq \dom(M_{ij}^{l})$ then $M_{ij}^{l+1}(0)$ is - $M_{ij}^{l}(1)$. Let $M_{ij}^{l}(1)= \left(\verb+Xp[i]+, a_{ij} , c_{ij} - \right)$. By construction $a_{ij}$ is $\min\{t' | t' > D_{ji}^c \land - (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$ and $c_{ij}$ is $\min\{k | - D_{ji}^k = a_{ij}\}$. Let us show $c_{ij}$ is equal to $\min\{k | D_{ji}^k > - D_{ji}^{l-1} \}$ further referred as $c'$. First we have $D_{ji}^{c_{ij}} = - a_{ij} > D_{ji}^c$. Since $c$ by definition is greater or equal to $l-1$ , - then $D_{ji}^{c_{ij}}> D_{ji}^{l-1}$ and then $c_{ij} \geq c'$. Next, since - $c$ is $l-1$, $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{c} \}$ and then $a_{ij} - \leq D_{ji}^{c'}$. Thus, $c_{ij} \leq c'$ and we can conclude as in the - previous part. +En particulier, on a $D_{ji}^{c'} \not \in \{D_{ji}^{c}+1,\ldots,l-1\}$. +On peut donc appliquer le troisième item de l'hypothèse d'induction pour déduire +$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ et on peut conclure. + +\item Si $\{0,1\} \subseteq \dom(M_{ij}^{l})$, alors $M_{ij}^{l+1}(0)$ vaut + $M_{ij}^{l}(1)$. Soit $M_{ij}^{l}(1)= \left(\verb+Xp[i]+, a_{ij} , c_{ij} + \right)$. Par construction, $a_{ij}$ vaut $\min\{t' | t' > D_{ji}^c \land + (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$ et $c_{ij}$ est $\min\{k | + D_{ji}^k = a_{ij}\}$. Montrons que $c_{ij}$ est égal à $\min\{k | D_{ji}^k > + D_{ji}^{l-1} \}$, noté plus tard $c'$. On a tout d'abord $D_{ji}^{c_{ij}} = + a_{ij} > D_{ji}^c$. Puisque $c$ par définition est supérieur ou égal à $l-1$, + alors $D_{ji}^{c_{ij}}> D_{ji}^{l-1}$ et donc $c_{ij} \geq c'$. Ensuite, puisque + $c=l-1$, $c'$ vaut $\min\{k | D_{ji}^k > D_{ji}^{c} \}$ et donc $a_{ij} + \leq D_{ji}^{c'}$. Ainsi, $c_{ij} \leq c'$ et on peut conclure comme dans la partie précédente. \end{itemize} -The case where the domain $\dom(M^l_{ij})$ is empty but the formula $\exists k -\, .\, k \geq l \land D_{ji}^k = l$ is established is equivalent to the second -case given above and then is omitted. +Le cas où le domaine $\dom(M^l_{ij})$ est vide mais où la formule $\exists k +\, .\, k \geq l \land D_{ji}^k = l$ est vraie est équivalent au second +cas ci-dessus et n'est pas présenté. -Secondly, let us focus on the formula~(\ref{eq:correct_retrieve}). At iteration -$l+1$, let $c'$ be defined as $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Two cases -have to be considered depending on whether $D_{ji}^{l}$ and $D_{ji}^{l-1}$ are -equal or not. +Concentrons nous sur la formule~(\ref{eq:correct_retrieve}). A l'itération +$l+1$, soit $c'$ défini par $c'=\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Deux cas peuvent +apparaître selon que $D_{ji}^{l}$ et $D_{ji}^{l-1}$ sont égaux ou non. \begin{itemize} -\item If $D_{ji}^{l} = D_{ji}^{l-1}$, since $D_{ji}^{c'} > D_{ji}^{l-1}$, then - $D_{ji}^{c'} > D_{ji}^{l}$ and then $c'$ is distinct from $l$. Thus, the SPIN - execution detailed above does not modify $Xd_{ji}^{l+1}$. It is obvious to - establish that $Xd_{ji}^{l+1} = Xd_{ji}^{l} = X_i^{D_{ji}^{l-1}} = +\item Si $D_{ji}^{l} = D_{ji}^{l-1}$, puisque $D_{ji}^{c'} > D_{ji}^{l-1}$, alors + $D_{ji}^{c'} > D_{ji}^{l}$ et donc $c'$ est différent de $l$. L'exécution de SPIN + ne modifie pas $Xd_{ji}^{l+1}$. On a ainsi $Xd_{ji}^{l+1} = Xd_{ji}^{l} = X_i^{D_{ji}^{l-1}} = X_i^{D_{ji}^{l}}$. -\item Otherwise $D_{ji}^{l}$ is greater than $D_{ji}^{l-1}$ and $c$ is thus $l$. - According to \Equ{eq:Mij0} we have proved, we have - $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$. Then the SPIN execution - detailed above assigns $X_i^{D_{ji}^{l}}$ to $Xd_{ji}^{l+1}$, which ends the - proof of (\ref{eq:correct_retrieve}). +\item Sinon, $D_{ji}^{l}$ et plus grand que $D_{ji}^{l-1}$ et $c$ est donc égal à $l$. + Selon l'équation \Equ{eq:Mij0}, on a + $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$. Ainsi l'exécution SPIN + affecte $X_i^{D_{ji}^{l}}$ à $Xd_{ji}^{l+1}$, ce qui termine la preuve +(\ref{eq:correct_retrieve}). \end{itemize} -We are left to prove the induction of the third part of the lemma. Let $k$, $k +Il reste à prouver la partie inductive de la troisième partie du lemme. +Soit $k$, $k \in S^{l+1}$. % and $\verb+k'+ = k-1$. -At the end of the first execution of the \verb+update_elems+ process, we have +A l'issue de la première exécutions +du processus \verb+update_elems+, on a $\verb+Xp[+k\verb+]+= F(\verb+Xd[+k\verb+][0]+, -\ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$. By definition of $Xd$, it is equal -to $F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$. Thanks to -\Equ{eq:correct_retrieve} we have proved, we can conclude the proof. +\ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$. +Par définition $Xd=F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$. +Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve. \end{Proof} @@ -284,7 +289,7 @@ to $F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$. Thanks to % performed under weak fairness property; we then detail what are continuously % enabled: % \begin{itemize} -% \item if the strategy is not defined as periodic, elements $0$, \ldots, $n$ are +% \item if the strategy is not defined as periodic, elements $0$, \ldots, $\mathsf{N}$ are % infinitely often updated leading to pseudo-periodic strategy; % \item instructions that write or read into \verb+channels[j].sent[i]+ are % continuously enabled leading to convenient available dates $D_{ji}$. diff --git a/demandeInscription/synthese.tex b/demandeInscription/synthese.tex index 03c44f7..58ad6b7 100755 --- a/demandeInscription/synthese.tex +++ b/demandeInscription/synthese.tex @@ -1557,10 +1557,9 @@ Jean-François Couchot, Raphaël Couturier, Yousra Ahmed Fadil and Christophe Gu Lisboa, Portugal, July 2016. \bibitem{kcm16:ip} -Nesrine Khernane, J.-F. Couchot, A. Mostefaoui. +N. Khernane, J.-F. Couchot, A. Mostefaoui. \newblock Maximizing Network Lifetime in Wireless Video Sensor Networks Under Quality Constraints. -\newblock In {\em The 19th ACM International Conference on Modeling, Analysis -and Simulation of Wireless and Mobile Systems, MSWiM'16} Malta, to appear, November, 2016. +\newblock In {\em MOBIWAC 2016: The 14th ACM* International Symposium on Mobility Management and Wireless Access} Malta, to appear, November, 2016. \bibitem{BCDG07} Fabrice Bouquet, Jean-Fran\c{c}ois Couchot, Fr\'ed\'eric Dadeau, and Alain diff --git a/main.tex b/main.tex index da87f22..33a3ba1 100644 --- a/main.tex +++ b/main.tex @@ -172,7 +172,7 @@ Blabla blabla. \mainmatter -\part{Réseaux Discrets} +\part{Réseaux discrets} \chapter{Iterations discrètes de réseaux booléens} @@ -182,8 +182,8 @@ les différents modes opératoires, leur représentation à l'aide de graphes et les résultats connus de convergence). Ce chapitre montre ensuite à la section~\ref{sec:sdd:mixage} comment combiner ces modes pour converger aussi -souvent sans, mais plus rapidement. Cette dernière section -a fait l'objet du rapport~\cite{BCVC10:ir}. +souvent, mais plus rapidement vers un point fixe. Les deux +dernières sections ont fait l'objet du rapport~\cite{BCVC10:ir}. \section{Formalisation}\label{sec:sdd:formalisation} \input{sdd} @@ -339,7 +339,7 @@ du chapitre 8} \appendix -\chapter{Preuves sur les SDD} +\chapter{Preuves sur les réseaux discrets} \section{Convergence du mode mixe}\label{anx:mix} \input{annexePreuveMixage} diff --git a/mixage.tex b/mixage.tex index e4a283c..4ee1171 100644 --- a/mixage.tex +++ b/mixage.tex @@ -21,9 +21,6 @@ s^{t}=24 \textrm{ si $t$ est pair et } s^{t}=15 \textrm{ sinon } \end{equation} \noindent active successivement les deux premiers éléments (24 est 11000) et les quatre derniers éléments (15 est 01111). -On dit que la stratégie est -\emph{pseudo-periodique} si tous les éléments sont activés infiniment -souvent. % , it is sufficient to establish that the set $\{t \mid t \in \mathbb{N} % \land \textit{bin}(s^t)[i] = 1\}$ is infinite for any $i$, $1 \le i \le n$, % where @@ -54,7 +51,7 @@ souvent. Dans le mode asynchrone, a chaque itération $t$, chaque composant peut mettre à jour son état en fonction des dernières valeurs qu'il connaît des autre composants. -Obtenir ou non les valeurs les plus à jours dépend du temps de calcul et +Obtenir ou non les valeurs les plus à jour dépend du temps de calcul et du temps d'acheminement de celles-ci. On parle de latence, de délai. Formalisons le mode les itérations asynchrone. @@ -190,7 +187,7 @@ Les itérations asynchrones sont conservées entre les groupes. La \emph{relation de synchronisation} $\eqNode$ est définie sur l'ensemble des n{\oe}uds par: $i \eqNode j$ si $i$ et $j$ appartiennent à la même composante fortement - connexe (CFC) dans $\Gamma(F)$. + connexe (CFC) dans $\Gamma(f)$. \end{Def} On peut facilement démontrer que la relation de synchronisation est une @@ -214,7 +211,7 @@ Ainsi $p_1$ et $p_2$ sont distinguables même s'ils appartiennent à la même classe. Pour gommer cette distinction, on définit le mode suivant: \begin{Def}[Itérations mixes avec delais uniformes] - Le mode mixe a des \emph{délais uniformes}si pour chaque + Le mode mixe a des \emph{délais uniformes} si pour chaque $t=0,1,\ldots$ et pour chaque paire de classes $(\class{p}, \class{q})$, il existe une constante $d^t_{pq}$ telle que la propriété suivante est établie: @@ -420,7 +417,7 @@ ascendants pour converger. On a dans ce cas: mode synchrone. \end{xpl} -\subsection{Le mode généralisé asynchrone} +\subsection{Le mode unaire asynchrone} \label{sec:evalasync} En terme de durée de convergence, ce mode peut être vu comme un cas particulier du mode mixe où toutes les classes sont des singletons. @@ -442,7 +439,7 @@ et apparaît lorsque chaque élément dépend des autres et que les calculs ne recouvrent nullement les communications. \begin{xpl} - La \Fig{fig:evalasync} présente un exemple d'exécution du mode généralisé + La \Fig{fig:evalasync} présente un exemple d'exécution du mode unaire asynchrone. Certaines communications issues de l'élément $4$ n'ont pas été représentées pour des raisons de clarté. diff --git a/modelchecking.tex b/modelchecking.tex index 2a7107f..b01a526 100644 --- a/modelchecking.tex +++ b/modelchecking.tex @@ -19,18 +19,19 @@ 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 +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 selon 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 @@ -38,8 +39,8 @@ 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}. @@ -88,11 +89,12 @@ Ce chapitre a fait l'objet du rapport~\cite{Cou10:ir}. -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} @@ -153,7 +155,7 @@ 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é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; @@ -208,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 @@ -218,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}$. @@ -343,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 @@ -588,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. @@ -650,7 +652,7 @@ 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)}$. @@ -667,7 +669,7 @@ 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} @@ -804,10 +806,7 @@ 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. @@ -818,7 +817,7 @@ L'exemple \textit{RE} a été prouvé comme universellement convergent. 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 diff --git a/sdd.tex b/sdd.tex index 69e09b6..c41efa9 100644 --- a/sdd.tex +++ b/sdd.tex @@ -30,7 +30,7 @@ et $\overline{x}^i$ pour $\overline{x}^{\{i\}}$ pour $i \in [{\mathsf{N}}]$ Pour tout $x$ et $y$ dans $\Bool^{\mathsf{N}}$, l'ensemble $\Delta(x, y)$, contient les $i \in [{\mathsf{N}}]$ tels que $x_i \neq y_i$. -Soit enfin $f : \Bool^n \rightarrow \Bool^{\mathsf{N}}$. Son $i^{\textrm{ème}}$ composant +Soit enfin $f : \Bool^{\mathsf{N}} \rightarrow \Bool^{\mathsf{N}}$. Son $i^{\textrm{ème}}$ composant est nommé $f_i$ qui est une fonction de $\Bool^{\mathsf{N}}$ dans $\Bool$. Pour chaque $x$ dans $\Bool^{\mathsf{N}}$, l'ensemble @@ -95,8 +95,8 @@ Pour $x=(0,1,0)$ les assertions suivantes se déduisent directement du tableau: \end{xpl} \subsection{Réseau booléen} -Soit $n$ un entier naturel représentant le nombre -d'éléments étudiés (gènes, protéines,\ldots). +Soit ${\mathsf{N}}$ un entier naturel représentant le nombre +d'éléments étudiés. Un réseau booléen est défini à partir d'une fonction booléenne: \[ @@ -118,7 +118,7 @@ schémas suivants : défini par une suite $S = \left(s^t\right)^{t \in \mathds{N}}$ qui est une séquence d'indices dans $[{\mathsf{N}}]$. Cette suite est appelée \emph{stratégie unaire}. - Il est basé sur la relation définie pour tout $i \in [{\mathsf{N}}]$ par + Ce mode est défini pour tout $i \in [{\mathsf{N}}]$ par \begin{equation} x^{t+1}_i= @@ -274,7 +274,7 @@ On a la proposition suivante: \begin{theorem}\label{Prop:attracteur} -Le point $x$ est un point fixe si et seulement si +La configuration $x$ est un point fixe si et seulement si $\{x\}$ est un attracteur du graphe d'itération (synchrone, unaire, généralisé). En d'autres termes, les attracteurs non cycliques de celui-ci sont les points fixes de $f$. @@ -331,7 +331,7 @@ $f'_{ij}(x)=0$. Ainsi $B(f)_{ij}$ est nulle. La réciproque est aussi vraie. En outre, les interactions peuvent se représenter à l'aide d'un graphe $\Gamma(f)$ orienté et signé défini ainsi: -l'ensemble des sommet %s est +l'ensemble des sommets est $[{\mathsf{N}}]$ et il existe un arc de $j$ à $i$ de signe $s\in\{-1,1\}$, noté $(j,s,i)$, si $f_{ij}(x)=s$ pour au moins un $x\in\Bool^{\mathsf{N}}$. @@ -527,22 +527,21 @@ Parmi toutes les stratégies unaires de $[{\mathsf{N}}]^{\Nats}$, on qualifie de: \begin{itemize} \item \emph{périodiques} celles -qui sont constituées par une répétition indéfinie +qui sont constituées par une répétition infinie d'une même séquence $S$ complète relativement à $[{\mathsf{N}}]$. En particulier toute séquence périodique est complète. \item \emph{pseudo-périodiques} celles -qui sont constituées par une succession indéfinie de séquences +qui sont constituées par une succession infinie de séquences (de longueur éventuellement variable non supposée bornée) complètes. Autrement dit dans chaque stratégie pseudo-périodique, chaque indice de -$1$ à ${\mathsf{N}}$ revient indéfiniment. +$1$ à ${\mathsf{N}}$ revient infiniment. \end{itemize} -François Robert~\cite{Rob95} -a énoncé en 1995 le théorème suivant de convergence +On a le théorème suivant de convergence dans le mode des itérations unaires. -\begin{theorem}\label{Th:conv:GIU} +\begin{theorem}[~\cite{Rob95}]\label{Th:conv:GIU} Si le graphe $\Gamma(f)$ n'a pas de cycle et si la stratégie unaire est pseudo-périodique, alors tout chemin de $\textsc{giu}(f)$ atteint l'unique point fixe $\zeta$ en au plus ${\mathsf{N}}$ pseudo-périodes. @@ -551,11 +550,11 @@ l'unique point fixe $\zeta$ en au plus ${\mathsf{N}}$ pseudo-périodes. Le qualificatif \emph{pseudo-périodique} peut aisément s'étendre aux stratégies généralisées comme suit. Lorsqu'une stratégie généralisée est constituée d'une -succession indéfinie de séquences de parties de $[{\mathsf{N}}]$ +succession infinie de séquences de parties de $[{\mathsf{N}}]$ dont l'union est $[{\mathsf{N}}]$, cette stratégie est {pseudo-périodique}. -J. Bahi~\cite{Bah00} a démontré le théorème suivant: +On a le théorème suivant. -\begin{theorem}\label{Th:Bahi} +\begin{theorem}[~\cite{Bah00}]\label{Th:Bahi} Si le graphe $\Gamma(f)$ n'a pas de cycle et si la stratégie généralisée est pseudo-périodique alors tout chemin de $\textsc{gig}(f)$ (et donc de $\textsc{giu}(f)$) diff --git a/stabylo.tex b/stabylo.tex index dda07a4..8801599 100644 --- a/stabylo.tex +++ b/stabylo.tex @@ -27,7 +27,7 @@ A partir de ces cartes de distortions, chacun de ces algorithmes selectionne les pixels dont les modifications induisent la distortion la plus faible possible. Ceci revient à définir une fonction de signification $u$. La complexité du schéma de stéganographie est peu ou prou celle du calcul -de cette carte, et elle est élevée (cf partie~\ref{XXXXXXXX}) dans le cas +de cette carte, et elle est élevée dans le cas de ces algorithmes. Nous avons proposé un algorithme~\cite{ccg15:ij} de complexité beaucoup plus faible diff --git a/stegoyousra.tex b/stegoyousra.tex index cfda20f..7f2add3 100644 --- a/stegoyousra.tex +++ b/stegoyousra.tex @@ -34,6 +34,7 @@ données et prouvées (Section~\ref{sec:second} et Section~\ref{sec:poly}). Une adaptation d'une fonction de distorsion existante est étudiée en Section~\ref{sec:distortion} et des expériences sont présentées en Section~\ref{sec:experiments}. +Ce chapitre a été publié dans~\cite{ccfg16:ip}. @@ -736,23 +737,16 @@ compte des variations dans celle-ci. Les dérivées secondes sont certes faciles %\end{figure} -% \section{Conclusion} - -% The first contribution of this paper is to propose of a distortion -% function which is based on second order derivatives. These -% partial derivatives allow to accurately compute -% the level curves and thus to look favorably on pixels -% without clean level curves. -% Two approaches to build these derivatives have been proposed. -% The first one is based on revisiting kernels usually embedded -% in edge detection algorithms. -% The second one is based on the polynomial approximation -% of the bitmap image. -% These two methods have been completely implemented. -% The first experiments have shown that the security level -% is slightly inferior the one of the most stringent approaches. These first promising results encourage us to deeply investigate this research direction. - -% Future works aiming at improving the security of this proposal are planned as follows. The authors want first to focus on other approaches to provide second order derivatives with larger discrimination power. -% Then, the objective will be to deeply investigate whether the H\"older norm is optimal when the objective is to avoid null second order derivatives, and to give priority to the largest second order values. - - +\section{Conclusion} +La principale contribution de ce chapitre est de proposer des +fonctions de distorsion basées sur des approximations de dérivées +secondes, l'idée sous-jacente étant qu'une zone où les lignes de niveau +ne sont pas clairement définies est peu prédictible. +Deux approches d'approximation ont été présentées. +La première basée +sur un produit de convolution, exploite des noyaux déjà intégrés dans des +algorithmes de détection de bords. +La seconde s'appuie sur une interpolation polynomiale de l'image. +Ces deux méthodes onté été complètement implantées et leur sécurité +face à des stéganalyseurs a été étudiée. Les résultats encouragent +à poursuivre dans cette direction. \ No newline at end of file -- 2.39.5