Infra
/
tiramisu
5
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

eole presentation

This commit is contained in:
gwen 2012-06-13 08:37:27 +02:00
parent e5bdb4c2ca
commit d5ef466350
2 changed files with 10 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
doc/eole-report/presentation/definition.tex
View File

@ -2,7 +2,7 @@
\frametitle{Gestionnaire de configuration existants} \frametitle{Gestionnaire de configuration existants}
\begin{itemize} \begin{itemize}
\item Le gestionnaire de conf de Victor Stinner $\Rightarrow$ \emph{NuFw}; \item Le gestionnaire de conf de Victor Stinner $\Rightarrow$ \emph{NuFw};
\item puppet, cfgengine... $\Rightarrow$ intéressant, de nombreux comportement peuvent être repris, mais tel quel difficilement compatible avec \emph{Creole}; \item puppet, cfgengine... $\Rightarrow$ intéressant, de nombreux comportements peuvent être repris, mais tel quel difficilement compatible avec \emph{Creole};
\item \emph{Creole} $\Leftrightarrow$ \texttt{tiramisu/doc/build/glossary.html} \item \emph{Creole} $\Leftrightarrow$ \texttt{tiramisu/doc/build/glossary.html}
\end{itemize} \end{itemize}
\end{frame} \end{frame}
@ -17,9 +17,9 @@
\item Et en plus : \item Et en plus :
\begin{itemize} \begin{itemize}
\item \emph{Créole} valide le type mais pas la structure (fait confiance au \texttt{XML}) ; \item \emph{Créole} valide le type mais pas la structure (fait trop confiance au \texttt{XML}) ;
\item \emph{Créole} difficile d'ajouter un type à cause de la métaclasse ; \item Avec \emph{Créole} il est compliqué d'ajouter un type à cause de la métaclasse ;
\item \emph{Tiramisu} valide le type \emph{et} la structure, ajout de types aisé. \item \emph{Tiramisu} valide le type \emph{et} la structure, et l'ajout de types est aisé.
\end{itemize} \end{itemize}
\item \texttt{eole-report/D02CoherenceVariables.pdf} \item \texttt{eole-report/D02CoherenceVariables.pdf}
\end{itemize} \end{itemize}

10
doc/eole-report/presentation/statut.tex
View File

@ -37,17 +37,18 @@
\begin{frame} \begin{frame}
\frametitle{un peu de mathématiques : prévenir les deadlocks} \frametitle{un peu de mathématiques : prévenir les deadlocks}
\begin{itemize} \begin{itemize}
\item sûreté : quelque chose de mauvais (deadlock) ne se produira pas \item sûreté : prévention des deadlocks ;
\item dans tiramisu, le modèle est suffisamment abstrait pour que son exploitation mathématique soit \item dans tiramisu, le modèle est suffisamment abstrait pour que son exploitation mathématique soit
réalisable par les techniques de \emph{Model Checking}; réalisable par les techniques de \emph{Model Checking} ;
\item soit on a besoin de ne connaître que l'ensemble des états, pas leurs liens $\Rightarrow$ espace d'états ; \item soit on a besoin de ne connaître que l'ensemble des états, pas leurs liens $\Rightarrow$ espace d'états ;
\item soit on a besoin de connaître toutes les relations $\Rightarrow$ graphe d'accessibilité ; \item soit on a besoin de connaître toutes les relations $\Rightarrow$ graphe d'accessibilité ;
\item la configuration peut alors être formalisée en une structures de \emph{Kripe} \item la configuration est modélisable en une structure de \emph{Kripe} ;
\item déjà le parsing de la conf est facile \texttt{tiramisu/report/build/index.html}
\end{itemize} \end{itemize}
\end{frame} \end{frame}
\begin{frame} \begin{frame}
\frametitle{un peu de mathématiques : le Model Checking} \frametitle{un peu de mathématiques (suite) CreoleLint}
\begin{itemize} \begin{itemize}
\item exemple : $ P = 3 \wedge Q = 1 \triangleleft \langle P = 1 \hookleftarrow Q = 0 \rangle$ \item exemple : $ P = 3 \wedge Q = 1 \triangleleft \langle P = 1 \hookleftarrow Q = 0 \rangle$
\item la propriété dans aucun état on a $P = 3$ et $Q = 1$ est-elle vraie ? \item la propriété dans aucun état on a $P = 3$ et $Q = 1$ est-elle vraie ?
@ -56,6 +57,7 @@ Pour vérifier cette propriété, on a besoin de connaître l'espace d'états ;
est-elle vraie ? Cela demande de connaître le graphe d'accessibilité : est-elle vraie ? Cela demande de connaître le graphe d'accessibilité :
\item les structures de \emph{Kripe} sont des machines à états étiquetées par les valuations de toutes les variables propositionnelles. \item les structures de \emph{Kripe} sont des machines à états étiquetées par les valuations de toutes les variables propositionnelles.
\item une compliation statique devient possible dans \emph{CreoleLint} \dots
\end{itemize} \end{itemize}
\end{frame} \end{frame}