talk/preuveconvmotiv.tex

   1
   2 \begin{itemize}
   3 \item Conditions suffisantes de convergence: facile à appliquer,
   4   domaine restreint.
   5 \item Recherche d'une métrique decroissante minorée: difficile.
   6 \item Simulations:
   7 \begin{itemize}
   8 \item Non exhaustives pour les schémas généralisés et asynchrones.
   9 \item Verdict $\leftrightarrow$ vérité ssi divergence (contre-exemple).
  10 \end{itemize}
  11 \item Souhait: exploiter un outil qui traiterait toutes les transitions.
  12 \begin{itemize}
  13 \item Explosion combinatoire: par abstraction,
  14   quotientage, ordre partiel\ldots
  15 \item Model checker: SPIN~\cite{Hol03}.
  16 \item Correction et complétude de la démarche.
  17   \end{itemize}
  18 \end{itemize}