diff options
| -rw-r--r-- | doc/soutenance/soutenance.tex | 303 |
1 files changed, 115 insertions, 188 deletions
diff --git a/doc/soutenance/soutenance.tex b/doc/soutenance/soutenance.tex index 905a6b6..1d57e21 100644 --- a/doc/soutenance/soutenance.tex +++ b/doc/soutenance/soutenance.tex @@ -12,6 +12,15 @@ \usetheme{Luebeck} \useoutertheme[footline=authortitle,subsection=false]{miniframes} +\addtobeamertemplate{navigation symbols}{}{% + \usebeamerfont{footline}% + \usebeamercolor[fg]{footline}% + \hspace{1em}% + \insertframenumber/\inserttotalframenumber +} +\setbeamercolor{footline}{fg=blue} +\setbeamerfont{footline}{series=\bfseries} + \usepackage{tikz} \usetikzlibrary{positioning} \usetikzlibrary{trees} @@ -34,9 +43,10 @@ % ----------------------- % entete -\title{Analyse statique de SCADE par interprétation abstraite} -\author{Alex AUVOLAT} -\date{Juillet 2014} +\title{Analyse statique de SCADE \\ par interprétation abstraite} +\subtitle{soutenance de stage} +\author[Alex AUVOLAT]{Alex AUVOLAT \\ {\small ANSYS-Esterel Technologies \\ sous l'encadrement de Jean-Louis Colaço}} +\date{Juin-Juillet 2014} \begin{document} @@ -46,9 +56,11 @@ \begin{frame}\frametitle{Introduction} \begin{itemize} - \item On cherche à vérifier des propriétés sur des programmes SCADE (propriétés générales ou propriétés spécifiées dans le code) - \item Différentes techniques d'analyse existent~: interprétation abstraite (Astrée), model checking (DV, Kind, GATeL) - \item Motivation~: en faisant l'analyse directement sur SCADE, on se passe d'un certain nombre de problèmes spécifiques à C (modèle mémoire, initialisation, ...) + \item SCADE~: programmation de systèmes embarqués critique + \item Forte motivation pour la vérification formelle + \item Techniques~: interprétation abstraite (Astrée), model checking (DV, Kind, GATeL) + \item Objectif du stage~: nouvelle technique d'analyse + \item Nombreux avantages à analyser directement le code SCADE \end{itemize} \end{frame} @@ -62,50 +74,57 @@ \section{Généralités sur SCADE} \frame{\sectionpage} +\begin{frame}[fragile]\frametitle{Programme synchrone} + \begin{itemize} + \item Le temps est discret + \item Toutes les variables évoluent en même temps + \end{itemize} + \begin{example} + \begin{verbatim} + x = 0 -> (pre y + 1) + y = x + 1 + \end{verbatim} + \end{example} +\end{frame} \begin{frame}\frametitle{Environnements mémoire} Soit un programme SCADE, on note~: \begin{itemize} - \item $\mathbb{X}$ l'ensemble de ses variables ; - \item $\mathbb{V}$ l'ensemble des valeurs qu'elles peuvent prendre. + \item $\mathbb{X}$~: ensemble des variables + \item $\mathbb{V}$~: ensemble des valeurs \end{itemize} + Ce modèle simple suffit ! \begin{definition} - Un envrionnement mémoire est une fonction de $\mathbb{X}\to\mathbb{V} = \mathbb{M}$ + Environnement mémoire~: fonction de $\mathbb{X}\to\mathbb{V} = \mathbb{M}$ \end{definition} - Dans notre étude, on est ammené à étudier des ensembles d'environnements mémoire, c'est-à-dire des éléments de $\mathcal{P}(\mathbb{M})$. - - On bénéficie de la structure de treillis de $(\mathcal{P}(\mathbb{M}), \emptyset, \mathbb{M}, \subseteq, \cup, \cap)$. \end{frame} \begin{frame}\frametitle{Système de transition, fonction de transition} Un programme SCADE représente une fonction de transition~: $$s_0 \xrightarrow{i_1} s_1 \xrightarrow{i_2} s_2 \xrightarrow{i_3} \cdots$$ - On peut réécrire cette sémantique de transition avec deux fonctions: $c$, qui copie une partie de $s_{n-1}$ dans $s_n$ pour garder des mémoires, et $f$ qui prend ces mémoires ainsi que les entrées pour calculer $s_n$: + Autre écriture~: $$s_n = f(c(s_{n-1}) + i_n)$$ \end{frame} \begin{frame}\frametitle{Sémantique collectrice} - On s'intéresse aux états du programme pour toutes les entrées possibles~: - $$g(A) = \{ f(c(s) + i), s \in A, i \in \mathbb{I} \}$$ - Puis on s'intéresse à tous les états du programme, à tous les cycles~: - $$S = lfp_{S_0} ( \lambda A. A \cup g(A) )$$ - $$S \in \mathcal{P}(\mathbb{M})$$ - Où $S_0$ est l'ensemble des états mémoire initiaux pour le programme. + \begin{itemize} + \item But~: prouver des propriétés générales + \item On considère ensemble toutes les entrées possible du programme (première abstraction) + \item On considère ensemble tous les moments de l'exécution du programme (seconde abstraction) + \item Sémantique collectrice~: $S \subset \mathcal{P}(\mathbb{M})$ + \item Elle peut s'exprimer comme un point fixe~: + $$S = lfp_{S_0} ( \lambda A. A \cup g(A) )$$ + \end{itemize} \end{frame} \begin{frame}\frametitle{Preuve de propriétés} - La sémantique collectrice $S$ représente une première abstraction de notre programme~: c'est l'ensemble de tous les états mémoire accessible par notre programme, quelque soient les entrées, et à tout moment de l'exécution. - - Prouver une propriété $P$, c'est montrer que $\forall s \in S, P(S)$. + Prouver une propriété $P$, c'est montrer que $\forall s \in S, s \models P$. \end{frame} \section{Interprétation abstraite} \frame{\sectionpage} \begin{frame}\frametitle{Abstraction} - Pour pouvoir travailler sur $\mathcal{P}(\mathbb{M})$ de manière algorithmique, c'est-à-dire faire une analyse qui termine, on procède par abstraction. - - Pour cela on représente les valeurs dans un domaine abstrait $\mathcal{D}^\sharp$. - \begin{definition} - Fonctions d'abstraction et de concretisation~: - $$\alpha: \mathcal{P}(\mathbb{M}) \to \mathcal{D}^\sharp$$ - $$\gamma: \mathcal{D}^\sharp \to \mathcal{P}(\mathbb{M})$$ - \end{definition} - Pour représenter $s \in \mathcal{P}(\mathbb{M})$, on utilise toujours une valeur abstraite $s^\sharp$ {\em sûre}, c'est-à-dire que $s \subset \gamma(s^\sharp)$. + \begin{itemize} + \item Pas d'algorithmes sur $\mathcal{P}(\mathbb{M})$ (problème de terminaison) + \item Domaine abstrait $\mathcal{D}^\sharp$~: représentation pouvant exprimer une classe d'éléments de $\mathcal{P}(\mathbb{M})$. + \item Fonction de concrétisation $\gamma$~: permet de comprendre ce que représente une valeur abstraite. + \item Abstraction sûre : $s^\sharp \models s \;\iff\; s \subset \gamma(s^\sharp)$ + \end{itemize} \end{frame} \begin{frame}\frametitle{Abstraction} \begin{figure} @@ -114,63 +133,23 @@ \input{alpha-gamma.pdf_tex} \end{figure} \end{frame} -\begin{frame}\frametitle{Structure de treillis} - On définit deux valeurs abstraites particulières~: - \begin{itemize} - \item $\bot$~: $\gamma(\bot) = \emptyset$ - \item $\top$~: $\gamma(\top) = \mathbb{M}$ - \end{itemize} - On définit également des opérateurs sur nos valeurs abstraites~: - \begin{itemize} - \item $\sqcup$~: $\gamma(s) \cup \gamma(s') \subset \gamma(s \sqcup s')$ - \item $\sqcap$~: $\gamma(s) \cap \gamma(s') \subset \gamma(s \sqcap s')$ - \end{itemize} - Ce qui munit $\mathcal{D}^\sharp$ d'une structure de treillis~: $(\mathcal{D}^\sharp, \bot, \top, \sqsubseteq, \sqcup, \sqcap)$. - - On cherche à chaque fois à trouver une meilleure approximation possible de $\gamma(s) \cup \gamma(s')$ ou $\gamma(s) \cap \gamma(s')$, sans jamais rien perdre (propriété de sûreté). -\end{frame} -\begin{frame}\frametitle{Abstraction non relationnelle} - On peut utiliser une abstraction qui traîte chaque variable séparément, en indiquant dans quel intervalle de valeurs elle évolue~: - $$\mathcal{D}^\sharp = \mathbb{X} \to itv(\mathbb{Z})$$ - ($itv(\mathbb{Z})$ est lui-même muni d'une structure de treillis) - \begin{example} - Par exemple si on a rencontré les environnements $\{x=0, y=5\}$ et $\{x=1, y=4\}$, on peut les représenter par la valeur abstraite $s$ telle que~: - $$s(x) = [0, 1]$$ - $$s(y) = [4, 5]$$ - \end{example} -\end{frame} -\begin{frame}\frametitle{Abstraction relationnelle} - On peut utiliser une abstraction qui mémorise des relations entre les variables. La plus célèbre est l'ensemble des polyèdres convexes, qui représente un ensemble d'environnements comme une conjonction d'égalités ou d'inégalités linéaires sur les variables. - \begin{example} - Par exemple si on a rencontré les environnements $\{x=0, y=5\}$ et $\{x=1, y=4\}$, on peut les représenter par la valeur abstraite $s$ qui contient les contraintes suivantes~: - $$0 \le x \le 1$$ - $$y = 5 - x$$ - \end{example} -\end{frame} -\begin{frame}\frametitle{Opérateur de widening} - L'opérateur de widening, habituellement noté $\nabla$, est un opérateur crucial pour faire terminer l'analyse des boucles. - - Pour les intervalles, il s'agit généralement d'envoyer une borne à l'infini~: - $$[1,3] \nabla [1,4] = [1, \infty]$$ - Pour les polyèdres, c'est plus complexe mais globalement cela peut se comprendre comme la suppression d'une ou de plusieurs contraintes. - - \begin{example} - Par exemple si on étudie un compteur qui est incrémenté à chaque tour de boucle, on va rencontrer les valeurs $x=1$, $x=2$, $x=3$, ... - - L'opérateur $\nabla$ permet d'extrapoler pour pouvoir dire~: $x$ varie dans $\mathbb{N}^*$. - \end{example} +\begin{frame}\frametitle{Domaines abstraits numériques} + \begin{itemize} + \item Plusieurs domaines bien connus~: intervalles, polyèdres, octogones. + \item Implémentation dans la bibliothèque Apron + \item Ne savent gérer que les variables numériques (entières ou rationnelles) + \end{itemize} \end{frame} \begin{frame}\frametitle{Abstraction de la sémantique collectrice, preuve de propriétés} - Si on souhaite prouver par exemple qu'une variable booléenne $p$ est toujours vraie, alors on a besoin de montrer que~: - $$\forall s \in S, s(p)=true$$ - - On ne peut pas manipuler $S$ directement, mais on peut en manipuler une abstraction $S^\sharp$ telle que $S \subset \gamma(S^\sharp)$. + \begin{itemize} + \item On abstrait $S$ par $S^\sharp$ tel que $S \subset \gamma(S^\sharp)$. - $S^\sharp$ est également défini comme un point fixe~: - $$S^\sharp = lfp_{S_0^\sharp} (\lambda s. s^\sharp \sqcup g^\sharp(s))$$ - - Si on montre que $p=true$ dans $S^\sharp$, c'est gagné. + \item $S^\sharp$ est également défini comme un point fixe~: + $$S^\sharp = lfp_{S_0^\sharp} (\lambda s. s^\sharp \sqcup g^\sharp(s))$$ + + \item Si on montre que $p=true$ dans $S^\sharp$, c'est gagné. + \end{itemize} \end{frame} \begin{frame}\frametitle{Preuve de propriété} \begin{figure} @@ -184,13 +163,11 @@ \frame{\sectionpage} \begin{frame}\frametitle{Besoin d'une abstraction performante} \begin{itemize} - \item On veut être capable de traîter correctement l'initialisation - \item On veut être capable d'étudier les états d'automates ou les branches de conditions séparément - \item On veut être capable d'utiliser des variables booléennes pour partitionner notre représentation abstraite + \item Problème~: le programme est considéré comme un seul lieu + \item On veut faire des disjonctions de cas + \item On veut étudier les conditions qui passent d'un cas à l'autre + \item En résumé~: notre programme encode un système de transitions (automate) \end{itemize} - Les domaines relationnels à base de polyèdres ou d'octogones ne sont pas à même de représenter des contraintes qui mettent en relation des variables énumérées et des variables numériques. - - Il a donc fallu développer de nouveaux domaines abstraits mieux adaptés. \end{frame} \begin{frame}[fragile]\frametitle{Un exemple} Étudions un programme simple~: @@ -205,33 +182,13 @@ On aimerait prouver $x \in [0,10]$ \end{frame} -\begin{frame}\frametitle{Itérations sur cet exemple} - Dans le cas où l'on ne fait pas de disjonctions, nos itérations vont ressembler à ça~: - \vspace{5mm} - - \begin{tabularx}{\linewidth}{|s|b|b|b|b|} - \hhline{-----} iter & \begin{bf}init\end{bf} & $\mathbf{lx}$ & $\mathbf{c}$ & $\mathbf{x}$ \\ - \hhline{|=|=|=|=|=|} - 0 & tt & 0 & ff & 1 \\ \hhline{-----} - 1 & $\top$ & $[0,1]$ & ff & $[1,2]$ \\ \hhline{-----} - 2 & $\top$ & $[0,2]$ & ff & $[1,3]$ \\ \hhline{-----} - 3 & $\top$ & $[0,3]$ & ff & $[1,4]$ \\ \hhline{-----} - 4 & $\top$ & $[0,\infty[$ & $\top$ & $[0,\infty[$ \\ \hhline{-----} - 5 & $\top$ & $[0,\infty[$ & $\top$ & $[0,\infty[$ \\ \hhline{-----} - \end{tabularx} - \vspace{5mm} - - On n'a pas réussi à prouver une borne supérieure sur $x$ ! -\end{frame} \begin{frame}\frametitle{Disjonctions de cas selon des variables} - On se done un ensemble $\mathbb{X}_d$ de variables énumérées (prenant leurs valeurs dans $\mathbb{V}_d$ un ensemble fini). - - On note $\mathbb{M}_d = \mathbb{X}_d \to \mathbb{V}_d$. - \begin{definition} - On définit le domaine abstrait suivant~: - $$\mathcal{D}^\sharp_d = \mathbb{M}_d \to \mathcal{D}^\sharp$$ - \end{definition} - Chaque combinaison possible pour les variables de $\mathbb{V}_d$ est traîtée séparément. En pratique tous les cas ne sont pas toujours accessibles. + \begin{itemize} + \item On se done un ensemble $\mathbb{X}_d$ de variables énumérées + \item On considère séparément chaque valuation de ces variables + $$\mathcal{D}^\sharp_d = \mathbb{M}_d \to \mathcal{D}^\sharp$$ + \item Chaque valuation correspond à un état du système de transition + \end{itemize} \end{frame} \begin{frame}\frametitle{Exemple} Une représentation appropriée pour traiter notre exemple serait~: @@ -247,30 +204,17 @@ \end{tabularx} \end{frame} -\begin{frame}\frametitle{Opérateurs correspondants} - La fonction de concrétisation donne la sémantique du domaine~: - $$\forall s \in \mathcal{D}_d^\sharp, \gamma(s) = \bigcup_{d\in\mathbb{M}_d} \left\{ e \in \gamma(s(d)) \;|\; \forall x \in \mathbb{X}_d, e(x)=d(x) \right\}$$ - - Si on considère une contrainte sur des variables énumérées du type $x \equiv y$, on est capable de la traîter comme suit~: - $$\llrrbracket{ x \equiv y}(s) - = \lambda d. - \begin{cases} s(d) & \text{si } d(x) = d(y) - \\ \bot & \text{sinon} - \end{cases}$$ - Les opérateurs $\sqcap, \sqcup$ et les valeurs $\top, \bot$ ne posent pas de problème. Par exemple, $s \sqcup s' = \lambda d. s(d) \sqcup s'(d)$. -\end{frame} \begin{frame}\frametitle{Principe d'itération} - On pourait faire des itérations globales sur notre environnement de $\mathcal{D}_d^\sharp$ jusqu'à trouver un point fixe, mais pour accélerer l'analyse et pour en améliorer la précision, on considère les cas un par un. + On construit $S^\sharp$ incrémentalement. \begin{itemize} - \item Prendre un cas nouveau - \item Rechercher un point fixe pour ce cas-là ; on profite alors des conditions qui font que l'on reste dans ce cas d'un cycle au suivant, à la manière de conditions de sortie de boucle, pour affiner l'analyse - \item Effectuer un cycle complet sans restriction, en partant de ce point fixe, et considérer tous les nouveaux cas que l'on a découvert + \item Prendre un cas nouveau $q$ + \item Étudier la boucle $q \to q$~: on trouve un point fixe précis + \item Étudier les nouveaux cas accessibles $q \to q'$. + \item Répéter \end{itemize} C'est le principe des {\em itérations chaotiques}. \end{frame} \begin{frame}\frametitle{Itérations chaotiques sur notre exemple} - Reprenons notre exemple. Maintenant, on a~: - \begin{tabularx}{\linewidth}{|su|b|b|b|b|} \hhline{------} & & \begin{bf}init\end{bf} & $\mathbf{lx}$ & $\mathbf{c}$ & $\mathbf{x}$ \\ \hhline{|==|=|=|=|=|} @@ -289,7 +233,7 @@ \end{tabularx} \end{frame} \begin{frame}\frametitle{Problème d'explosion} - On peut avoir à représenter des valeurs abstraites comme la suivante~: + On est souvent confronté à des représentations comme celle-ci~: \vspace{5mm} \begin{tabularx}{\linewidth}{|t|t|t|b|} @@ -335,20 +279,15 @@ \end{frame} \begin{frame}\frametitle{Disjonctions de cas avec graphe de décision} - On numérote les variables de $\mathbb{V}_d$~: $x_1, x_2, \dots, x_m$. - - On considère un type somme qui représente un graphe de décision~: - $$ \begin{tabular}{rcl} - T & := & V(s), s \in \mathcal{D}^\sharp \\ - & | & C(x_i, v_1 \to T_1, \dots, v_k \to T_k) - \end{tabular} $$ - La sémantique est donnée par la fonction de concrétisation~: - $$ \begin{tabular}{rcl} - \gamma(V(s)) & = & \gamma(s) \\ - \gamma(C(x, v_1 \to T_1, \dots, v_k \to T_k) & = & - \bigcup_{i=1}^k \{ e \in \gamma(T_i) \;|\; e(x) = v_i \} - \end{tabular} $$ - On impose que si un noeud $C(x_i, \dots)$ est parent d'un noeud $C(x_j, \dots)$, alors $i < j$, ce qui implique l'unicité de l'arbre. + \begin{itemize} + \item Graphe de décision, représenté par un type somme~: + $$ \begin{tabular}{rcl} + T & := & V(s), s \in \mathcal{D}^\sharp \\ + & | & C(x_i, v_1 \to T_1, \dots, v_k \to T_k) + \end{tabular} $$ + \item Unicité de la représentation garantie par une condition simple + \item Le partage de sous-graphes permet de gagner en compacité + \end{itemize} \end{frame} \begin{frame}[fragile]\frametitle{Retour à notre exemple} Notre exemple peut être représenté par la structure suivante~: @@ -388,41 +327,44 @@ \end{tikzpicture} \end{figure} \end{frame} -\begin{frame}\frametitle{Opérateurs correspondants} - \begin{itemize} - \item On fait du partage sur les feuilles et les sous-arbres identique, ce qui transforme notre structure en un DAG. - \item Les opérateurs $\sqcup$ et $\sqcap$ sont implémentés par récurrence, mais il faut utiliser une procédure de mémoisation pour éviter que la complexité soit exponentielle (on profite du partage). - \item L'application d'une condition sur les énumérés $x \equiv y$ s'effectue en faisant le $\sqcap$ avec un graphe qui représente cette contrainte. - \end{itemize} -\end{frame} \begin{frame}\frametitle{Principe d'itération} - On pourait de même faire des itérations globales, mais on a préféré implémenter les itérations chaotiques pour les mêmes raisons. - - Pour identifier les différents cas, on utilise la fonction suivante, qui extrait d'un graphe la fonction booléenne sur les variables énumérées qui mène à une feuille $V(s_0)$ (partagée)~: - $$ \begin{tabular}{rcl} - \rho(V(s), s_0) & = & \begin{cases} \top & \text{si } s = s_0 \\ \bot & \text{sinon} \end{cases} \\ - \rho(C(x_i, v_1 \to T_1, \dots), s_0) & = & C(x_i, v_1 \to \rho(T_1, s_0), \dots) - \end{tabular}$$ + \begin{itemize} + \item Problème~: un cas ne correspond plus à une valuation des variables $\mathbb{X}_d$. Que faire ? + \item On définit un cas comme étant tous les chemins menant à une feuille donnée. + \end{itemize} \end{frame} - - -\section{Résultats et conclusion} +\section{Contribution personnelle} \frame{\sectionpage} +\begin{frame}\frametitle{Contribution théorique} + \begin{itemize} + \item Formalisation de la sémantique concrète de SCADE (d'un sous-ensemble) + \item Représentation d'un programme SCADE sous la forme d'une formule logique, adaptée pour l'interprétation abstraite + \item Domaine abstrait à base de graphes de décision et itérations chaotiques associées + \end{itemize} +\end{frame} +\begin{frame}\frametitle{Implémentation} + \begin{itemize} + \item Sélection d'un sous-ensemble de SCADE + \item Implémentation d'un interprète concret + \item Implémentation de la transformation en formule logique + \item Implémentation du domaine abstrait à disjonction de cas de façon naïve + \item Ré-implémentation avec les graphes de décision + \end{itemize} +\end{frame} \begin{frame}\frametitle{Comparaison avec Astrée} \begin{itemize} - \item Astrée implémente un domaine abstrait permettant de traiter différents cas dans un arbre de disjonctions, mais les feuilles de cet arbre ne peuvent être que des intervalles de valeurs (ils ne gèrent pas les relations entre les variables). En conséquence, une propriété comme celle du double updown est difficile à montrer. - \item Dans Astrée, les variables sont considérées par {\em packs}. Pour les octogones, des packs sont générés automatiquement. Pour l'arbre de disjonctions, il faut spécifier manuellement que l'on veut que l'analyseur considère un pack comportant telles et telles variables. (L'ensemble des propriétés prouvées est la conjonction des propriétés prouvées à l'aide de chaque pack). - \item Astrée travaille sur du C, et se pose des questions inutiles (typiquement les questions d'initialisation ou de bornes) + \item Astrée~: analyse de C généré par SCADE. + \item Astrée n'implémente pas d'itérations chaotiques~: ça ne convient pas du tout à l'analyse de C + \item Astrée implémente un domaine avec des graphes de décision, mais il est moins puissant. + \item Astrée implémente de nombreuses techniques permettant de travailler sur de gros programmes (en particulier le variable packing) + \item Astrée se pose des questions inutiles en SCADE (typiquement les questions d'initialisation de mémoire) \end{itemize} \end{frame} -\begin{frame}\frametitle{Implémentation} - $\exists$ prototype. -\end{frame} \begin{frame}\frametitle{Résultats} - Plein de preuves sympathiques~: + Quelques programmes sur lesquels j'ai pu prouver des propriétés intéressantes~: \begin{itemize} \item compteurs \item updown @@ -432,21 +374,6 @@ \item un demi-tour pour des rames de metro \cite{lesartse} \end{itemize} \end{frame} -\begin{frame}\frametitle{Limitations} - \begin{itemize} - \item Pour certains problèmes, il faut rajouter manuellement des variables booléennes pour faire des disjonctions de cas - \item On ne sait pas comment ça se comporte sur des gros programmes - \item Aucune analyse des propriétés des nombres flottants - \item Analyseur non vérifié~: il manque quelques preuves concernant les abstractions (structures de treillis, connection de Galois, correction et terminaison des principes d'itérations chaotiques) - \end{itemize} -\end{frame} -\begin{frame}\frametitle{Perspectives} - \begin{itemize} - \item Développement d'une heuristique qui détermine quelles variables représentent la structure de contrôle du programme et sont pertinentes à considérer - \item Partitionnement dynamique - \item Analyses par packs de variables, comme Astrée - \end{itemize} -\end{frame} \begin{frame}\frametitle{Références} \bibliographystyle{apacite} \bibliography{research} |