\nonstopmode
\documentclass{beamer}
\usepackage[utf8]{inputenc}
\usepackage[francais]{babel}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{graphicx}
\usepackage{hhline}
\usepackage{caption}
\usepackage[notocbib]{apacite}
\usetheme{Luebeck}
\useoutertheme[footline=authortitle,subsection=false]{miniframes}
\usepackage{tikz}
\usetikzlibrary{positioning}
\usetikzlibrary{trees}
\tikzstyle{level 1}=[level distance=2cm, sibling distance=5.2cm]
\tikzstyle{level 2}=[level distance=1.7cm, sibling distance=2.6cm]
\tikzstyle{var}=[circle, draw=black, thick, text centered]
\tikzstyle{end}=[draw=black, thick, text centered]
\usepackage{tabularx}
\newcolumntype{b}{X}
\newcolumntype{s}{>{\hsize=.5\hsize}X}
\newcolumntype{t}{>{\hsize=.3\hsize}X}
\newcolumntype{u}{>{\hsize=.1\hsize}X}
\newcommand{\heading}[1]{\multicolumn{1}{|c}{#1}}
\newcommand{\llrrbracket}[1]{% \llrrbracket{..}
\left[\mkern-3mu\left[#1\right]\mkern-3mu\right]}
\usepackage{multicol}
% -----------------------
% entete
\title{Analyse statique de SCADE par interprétation abstraite}
\author{Alex AUVOLAT}
\date{Juillet 2014}
\begin{document}
\begin{frame}
\titlepage
\end{frame}
\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, ...)
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Plan}
\tableofcontents
\end{frame}
% ----------------------
% contenu
\section{Généralités sur SCADE}
\frame{\sectionpage}
\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.
\end{itemize}
\begin{definition}
Un envrionnement mémoire est une 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$:
$$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.
\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)$.
\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)$.
\end{frame}
\begin{frame}\frametitle{Abstraction}
\begin{figure}
\centering
\def\svgwidth{.9\textwidth}
\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}
\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)$.
$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é.
\end{frame}
\begin{frame}\frametitle{Preuve de propriété}
\begin{figure}
\centering
\def\svgwidth{.75\textwidth}
\input{property.pdf_tex}
\end{figure}
\end{frame}
\section{Domaines à disjonction de cas}
\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
\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~:
\vspace{7mm}
\begin{verbatim}
lx = 0 -> pre x
c = (lx >= 10)
x = if c then 0 else lx + 1
\end{verbatim}
\vspace{7mm}
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.
\end{frame}
\begin{frame}\frametitle{Exemple}
Une représentation appropriée pour traiter notre exemple serait~:
\vspace{5mm}
\begin{tabularx}{\linewidth}{|s|s|b|}
\hline \begin{bf}init\end{bf} & $\mathbf{c}$ & \\
\hhline{|=|=|=|}
tt & tt & $\bot$ \\ \hline
tt & ff & $lx = 0; x = 1$ \\ \hline
ff & tt & $lx = 10; x = 0$ \\ \hline
ff & ff & $0 \le lx \le 9; x = lx + 1$ \\ \hline
\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.
\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
\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{|==|=|=|=|=|}
0 & $\star$ & tt & 0 & ff & 1 \\ \hhline{------}
1 & & $tt$ & $0$ & ff & $1$ \\ \hhline{|~~|----}
& $\star$ & $ff$ & $1$ & ff & $2$ \\ \hhline{------}
2 & & $tt$ & $0$ & ff & $1$ \\ \hhline{|~~|----}
& & $ff$ & $[1,9]$ & ff & $[2,10]$ \\ \hhline{|~~|----}
& $\star$ & $ff$ & $10$ & tt & 0 \\ \hhline{------}
3 & & $tt$ & $0$ & ff & $1$ \\ \hhline{|~~|----}
& $\star$ & $ff$ & $[0,9]$ & ff & $[1,10]$ \\ \hhline{|~~|----}
& & $ff$ & $10$ & tt & 0 \\ \hhline{------}
4 & & $tt$ & $0$ & ff & $1$ \\ \hhline{|~~|----}
& & $ff$ & $[0,9]$ & ff & $[1,10]$ \\ \hhline{|~~|----}
& & $ff$ & $10$ & tt & 0 \\ \hhline{------}
\end{tabularx}
\end{frame}
\begin{frame}\frametitle{Problème d'explosion}
On peut avoir à représenter des valeurs abstraites comme la suivante~:
\vspace{5mm}
\begin{tabularx}{\linewidth}{|t|t|t|b|}
\hhline{----} \begin{bf}init\end{bf} & $\mathbf{la}$ & $\mathbf{lb}$ & \\
\hhline{|=|=|=|=|}
tt & tt & tt & $a = 0; b = 0$ \\ \hhline{----}
tt & tt & ff & $a = 0; b = 0$ \\ \hhline{----}
tt & ff & tt & $a = 0; b = 0$ \\ \hhline{----}
tt & ff & ff & $a = 0; b = 0$ \\ \hhline{----}
ff & tt & tt & $a = 0; b \in [1, \infty[$ \\ \hhline{----}
ff & tt & ff & $a = 1; b \in [1, \infty[$ \\ \hhline{----}
ff & ff & tt & $a = -1; b \in [1, \infty[$ \\ \hhline{----}
ff & ff & ff & $a = 0; b \in [1, \infty[$ \\ \hhline{----}
\end{tabularx}
\vspace{5mm}
Il y a beaucoup de redondance !
\end{frame}
\begin{frame}\frametitle{La solution}
\begin{figure}\centering
\begin{tikzpicture}[->]
\node[var, text centered] (init) {init};
\node[var, below right = .7cm and 1.5cm of init] (la) {la};
\node[var, below left = .7cm and .4cm of la] (lb1) {lb};
\node[var, below right = .7cm and .4cm of la] (lb2) {lb};
\node[end, below left = 1cm and .4cm of lb1] (f2) {$\begin{tabular}{c}a = -1\\b \in [1,\infty[\end{tabular}$};
\node[end, right = .5cm of f2] (f3) {$\begin{tabular}{c}a = 0\\b \in [1, \infty[\end{tabular}$};
\node[end, below right = 1cm and .4cm of lb2] (f4) {$\begin{tabular}{c}a = 1\\b \in [1, \infty[\end{tabular}$};
\node[end, left = .6cm of f2] (f1) {$\begin{tabular}{c}a = 0\\b = 0\end{tabular}$};
\path[->, thick]
(init) edge node [left] {$tt$} (f1)
edge node [right] {$ff$} (la)
(la) edge node[left] {$ff$} (lb1)
edge node[right] {$tt$} (lb2)
(lb1) edge node[left] {$tt$} (f2)
edge node[right] {$ff$} (f3)
(lb2) edge node[left] {$tt$} (f3)
edge node[right] {$ff$} (f4)
\end{tikzpicture}
\end{figure}
\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.
\end{frame}
\begin{frame}[fragile]\frametitle{Retour à notre exemple}
Notre exemple peut être représenté par la structure suivante~:
\begin{figure}\centering
\begin{tikzpicture}[->,thick]
\node[var] {init}
child {
node[var] {c}
child {
node[end] {$\bot$}
edge from parent
node[left]{tt}
}
child {
node[end] {$\begin{tabular}{c}lx = 0 \\ x = 1\end{tabular}$}
edge from parent
node[right]{ff}
}
edge from parent
node[left] {tt}
}
child {
node[var] {c}
child {
node[end] {$\begin{tabular}{c}lx = 10 \\ x = 0\end{tabular}$}
edge from parent
node[left]{tt}
}
child {
node[end] {$\begin{tabular}{c}0 \le lx \le 9 \\ x = lx + 1\end{tabular}$}
edge from parent
node[right]{ff}
}
edge from parent
node[right] {ff}
};
\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}$$
\end{frame}
\section{Résultats et conclusion}
\frame{\sectionpage}
\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)
\end{itemize}
\end{frame}
\begin{frame}\frametitle{Implémentation}
$\exists$ prototype.
\end{frame}
\begin{frame}\frametitle{Résultats}
Plein de preuves sympathiques~:
\begin{itemize}
\item compteurs
\item updown
\item double updown
\item suite de cartes
\item un train \cite{halbwachs94c}
\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}
\end{frame}
\end{document}
