talk/sdd2promela.tex

   1 \begin{itemize}
   2 \item Points clefs de la traduction:
   3 \begin{itemize}
   4 \item Stratégie: pseudo périodicité garantie par le choix indéterministe de
   5   SPIN.
   6 \item Délais (bornés par construction): oubli de certaines valeurs grâce à l'indéterminisme de SPIN.
   7 \end{itemize}
   8 \item Convergence universelle:   $\diamond  (\Box  \verb+Xp+ = \verb+X+)$.
   9
  10
  11 \begin{theorem}[Correction et complétude de la traduction vers Promela~\cite{Cou10:ir}]
  12   Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.
  13   Les itérations de $\phi$ sont universellement convergentes si et
  14   seulement si
  15   $\psi$ vérifie
  16   la propriété  LTL  sous hypothèse d'équité faible.
  17 \end{theorem}
  18
  19 % \item Equité faible grantie uniquement entre processus:
  20 % \begin{itemize}
  21 % \item L'imposer pour chaque choix où
  22 % \item Filtrer les traces non équitables retournée.
  23 % \end{itemize}
  24 \item Bilan:
  25 \begin{itemize}
  26 \item Preuve automatique de convergence de modèles indpt. schéma/mode.
  27 \item A pu décider de la convergence d'exemples simples.
  28 \item Ne passe pas à l'échelle.
  29 \end{itemize}
  30 \end{itemize}