From 2073dd00710add906cc94099cd4bfb7aa3a2f85e Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 23 Jul 2014 18:03:28 +0200 Subject: Move README && add stuff ; add presentation. --- doc/prez/Makefile | 8 + doc/prez/alpha-gamma.svg | 266 +++++++ doc/prez/prez.pdf | Bin 0 -> 259816 bytes doc/prez/prez.tex | 456 +++++++++++ doc/prez/property.svg | 280 +++++++ doc/prez/research.bib | 21 + doc/readme.pdf | Bin 0 -> 236320 bytes doc/readme.tm | 1936 ++++++++++++++++++++++++++++++++++++++++++++++ 8 files changed, 2967 insertions(+) create mode 100644 doc/prez/Makefile create mode 100644 doc/prez/alpha-gamma.svg create mode 100644 doc/prez/prez.pdf create mode 100644 doc/prez/prez.tex create mode 100644 doc/prez/property.svg create mode 100644 doc/prez/research.bib create mode 100644 doc/readme.pdf create mode 100644 doc/readme.tm (limited to 'doc') diff --git a/doc/prez/Makefile b/doc/prez/Makefile new file mode 100644 index 0000000..89cfc3a --- /dev/null +++ b/doc/prez/Makefile @@ -0,0 +1,8 @@ +IMG=alpha-gamma.pdf_tex property.pdf_tex + + +prez.pdf: prez.tex $(IMG) + pdflatex prez.tex -halt-on-error -file-line-error + +%.pdf_tex: %.svg + inkscape -z -D --file=$< --export-pdf=$(basename $@).pdf --export-latex diff --git a/doc/prez/alpha-gamma.svg b/doc/prez/alpha-gamma.svg new file mode 100644 index 0000000..320ec14 --- /dev/null +++ b/doc/prez/alpha-gamma.svg @@ -0,0 +1,266 @@ + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + \huge concret + \huge abstrait + + + + + + + \Large $\alpha$ + \Large $\gamma$ + + + \scriptsize Exécutions du programme + + \scriptsize Sur-approximation + + \scriptsize Représentation abstraite + + diff --git a/doc/prez/prez.pdf b/doc/prez/prez.pdf new file mode 100644 index 0000000..251c931 Binary files /dev/null and b/doc/prez/prez.pdf differ diff --git a/doc/prez/prez.tex b/doc/prez/prez.tex new file mode 100644 index 0000000..905a6b6 --- /dev/null +++ b/doc/prez/prez.tex @@ -0,0 +1,456 @@ +\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} diff --git a/doc/prez/property.svg b/doc/prez/property.svg new file mode 100644 index 0000000..a3d085c --- /dev/null +++ b/doc/prez/property.svg @@ -0,0 +1,280 @@ + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + \large $P$ + + \large $P$ + + + $S$ + $S^\sharp$ + $S$ + $S^\sharp$ + + diff --git a/doc/prez/research.bib b/doc/prez/research.bib new file mode 100644 index 0000000..95acb0c --- /dev/null +++ b/doc/prez/research.bib @@ -0,0 +1,21 @@ + + @INPROCEEDINGS{halbwachs94c, + AUTHOR={N. Halbwachs}, + TITLE={About synchronous programming and abstract interpretation}, + BOOKTITLE={International Symposium on Static Analysis, SAS'94}, + EDITOR = {B. {LeCharlier}}, + PUBLISHER = {LNCS 864, Springer Verlag}, + ADDRESS = {Namur (belgium)}, + MONTH = {September}, + YEAR= 1994 +} +@ARTICLE{lesartse, + AUTHOR = {N. Halbwachs and F. Lagnier and C. Ratel }, + TITLE = {Programming and verifying real-time systems by means of + the synchronous data-flow programming language Lustre}, + JOURNAL = {IEEE Transactions on Software Engineering, + Special Issue on the Specification and Analysis + of Real-Time Systems}, + MONTH={September }, + YEAR=1992 +} diff --git a/doc/readme.pdf b/doc/readme.pdf new file mode 100644 index 0000000..4a97029 Binary files /dev/null and b/doc/readme.pdf differ diff --git a/doc/readme.tm b/doc/readme.tm new file mode 100644 index 0000000..8622a9a --- /dev/null +++ b/doc/readme.tm @@ -0,0 +1,1936 @@ + + + + +<\body> + |> + + + + Le projet consiste en la réalisation d'un analyseur statique pour des + programmes SCADE, utilisant l'interprétation abstraite comme base de + travail. Les objectifs attendus sont : + + <\itemize> + Preuve de propriétés de sûreté sur des programmes + + Étude d'intervalles de variation pour des variables + + + L'expérience a été menée sur un sous-ensemble très restreint du langage + SCADE, comportant notamment : + + <\itemize> + noyau dataflow (opérations arithmétiques élémentaires, opérateurs + > et ), pas de prise en charge des + horloges explicites (primitives , , ...) + + blocs + + automates simples, à transitions faibles seulement, sans actions + sur les transitions (les transitions de type sont + prises en compte) + + + Dans ce document nous mettrons au clair les points suivants : + + <\enumerate> + Spécification du sous-ensemble de SCADE considéré + + Explication du fonctionnement de l'interprète pour la sémantique + concrète + + Explication de la traduction d'un programme SCADE en une formule + logique représentant le cycle du programme + + Explications sur l'interprétation abstraite en général, sur les + domaines numériques, sur la recherche de points fixe + + Explications sur notre adaptation de ces principes à l'analyse du + langage SCADE, en particulier : + + <\itemize> + itérations chaotiques + + domaines capables de faire des disjonctions de cas (graphes de + décision) + + + + Par la suite, nous ne considérons que des programmes SCADE bien typés. + + + + + + <\verbatim-code> + <\verbatim> + decl \ \ \ := CONST id: type = expr; + + \ \ \ \ \ \ \ \ \ \| NODE (var_def;*) RETURNS (var_def;*) VAR var_def;* + body + + var_def := (PROBE? id),* : type + + body \ \ \ := LET eqn;* TEL + + \ \ \ \ \ \ \ \ \ \| eqn; + + type \ \ \ := INT \| BOOL \| REAL \| (TYPE,+) + + eqn \ \ \ \ := id = expr + + \ \ \ \ \ \ \ \ \ \| GUARANTEE id : expr + + \ \ \ \ \ \ \ \ \ \| ASSUME id : expr + + \ \ \ \ \ \ \ \ \ \| AUTOMATON state* RETURNS id,* + + \ \ \ \ \ \ \ \ \ \| ACTIVATE scope_if RETURNS id,* + + scope_if := (VAR var_def;*)? body + + \ \ \ \ \ \ \ \ \ \| IF expr THEN scope_if ELSE scope_if + + state \ \ \ := INITIAL? STATE id + + \ \ \ \ \ \ \ \ \ \ \ \ \ body + + \ \ \ \ \ \ \ \ \ \ \ \ \ until* + + until \ \ \ := UNTIL IF expr (RESUME\|RESTART) id + + expr \ \ \ \ := int_const \| real_const \| TRUE \| FALSE \| id + + \ \ \ \ \ \ \ \ \ \ \| unary_op expr \| expr bin_op expr + + \ \ \ \ \ \ \ \ \ \ \| IF expr THEN expr ELSE expr + + \ \ \ \ \ \ \ \ \ \ \| id ( expr,* ) + + unary_op := - \| PRE \| NOT + + bin_op \ \ := + \| - \| * \| / \| -\ \| AND \| OR \| MOD + + + \ \ \ \ \ \ \ \ \ \ \| = \| \\ \| \ \| \ \| + \= \| \= + + + + + Pour simplifier, on considère dans cette section que tous les noeuds ont + été inlinés. + + On note > l'ensemble des variables définies dans le texte du + programme, et on note > l'ensemble des valeurs qui peuvent + être prises. + + Un environnement de valeurs est une fonction + \\> qui décrit un état de la mémoire + du programme. On définit aussi un sous-ensemble + \\> de variables dont les valeurs + sont des entrées du système. + + L'exécution d'un programme est une séquence d'états mémoire + \,s,\,s,\> + conforme à la spécification du programme et à une série d'entrées. On note + : + + <\equation*> + s|i>s|i>s\\ + + + Dans la sémantique par traduction, la sémantique d'un programme est définie + par traduction du programme en une formule logique telle + que : + + <\eqnarray*> + |i>s>|>|x\\,s=i>>|,s|)>>>>>>>>>> + + + Dans la sémantique par réduction, la sémantique d'un programme est définie + par un ensemble de règles de réduction qui aboutissent à + + <\eqnarray*> + |i>s>|>|\i|s\s>>>>> + + + Pour un programme bien typé, étant donné > et + >, il existe un unique état > qui remplit la + condition. + + Un scope > correspond à un ensemble de définitions (de + variables, d'automates, ou de blocs activate), identifiés par un chemin. + Chaque scope dispose d'une horloge propre. Pour traduire l'init et le + reset, on introduit dans chaque scope > plusieurs variables + : + + <\itemize> + >> : indique que le scope devra être + reset lors du prochain cycle + + >> : indique que le scope est à l'état + initial dans ce cycle + + >> : indique qu'un scope est actif dans ce + cycle + + + Un nouveau scope est introduit dans chaque body d'un bloc activate ou d'un + état d'automate. + + De même, les automates introduisent deux variables :\ + + <\itemize> + >, qui définit l'état de l'automate à ce cycle + + >, qui définit l'état de l'automate au cycle + suivant, en supposant qu'il n'y a pas de reset du scope où l'automate est + défini + + + L'état > est défini par |)>=tt>, + où est le scope racine englobant tout le programme ; toutes les + autres variables de > pouvant prendre n'importe quelle + valeur. + + On suppose que chaque instance de est numérotée. Pour chaque + e>, on introduit la variable > qui + enregistre la valeur de dans le cycle courant et qui sert de + mémoire pour le pre lors du cycle suivant. + + Par la suite, que ce soit dans l'étude de la sémantique par réduction ou + par traduction, on notera toujours la mémoire (c'est-à-dire + >) et l'état courant (c'est-à-dire + >, sur lequel on travaille). + + + + On définit notre ensemble d'environnements comme étant + \\\|}>>, la + valeur > signifiant qu'une variable n'a pas encore pris sa + valeur. + + Pour chaque élément de programme, on va introduire un certain nombre de + règles de réduction. On applique ces règles jusqu'à en déduire + s>, avec x\\,s\\>. + + Les déductions de la forme s> signifient \S avec la + mémoire , on peut déduire du système l'état (partiel) \T. + Les déductions de la forme e\>v> + signifient \S avec la mémoire et l'état partiellement calculé + , l'expression calculée dans le scope > + prend la valeur \T (la flèche >> + correspond à une réduction par valeur dans le scope >). + + On notera \x=e> pour signifier \S dans le scope + > on a la définition \T, de même pour les + définitions de blocs activate et d'automates. On notera + \pre e> pour signifier que + e> apparaît dans le scope >. + + + + On note les entrées du système à ce cycle ; on fait par définition + l'hypothèse i>, c'est-à-dire qu'on peut obtenir + l'environnement où seules les variables d'entrée sont définies. On + introduit ensuite la règle suivante, qui dit que le scope racine est + toujours actif et jamais reset par la suite : + + <\equation*> + s|l\s\tt|]>\ff|]>> + + + \; + + + + Pour tout scope > défini dans le programme, qui est reset si + et seulement si la condition r> est vraie, on rajoute les + règles de réduction suivantes qui permettent de déterminer si le scope est + init ou pas : + + <\equation*> + s>||r>>>>>>|l\s>\tt|]>> + + + <\equation*> + s>||\r>>||>|)>=tt>>>>>|l\s>\ff|]>> + + + <\equation*> + s>||\r>>||>|)>=ff>>>>>|l\s>\l>|)>|]>> + + + \; + + En particulier, pour le scope racine on instancie ces règles avec + r|)>\l|)>=tt> + + + + Ces règles permettent d'exprimer le calcul d'une expression. On note + > le scope dans lequel l'expression est évaluée. On note + > n'importe quel opérateur binaire : + ,/,mod,\,\,\,\,=,\,\,\>. + + <\eqnarray*> + c\>c>,c\\>||\\|l,s\x\>s>,x\\>>>> + + + <\equation*> + pre e\>l|)>> + + + <\equation*> + e\>v>||e\>v>>>>>|l,s\e\e\>v\v> + + + <\eqnarray*> + >|)>=tt>||e\>v>>>>>|l,s\\e|)>\>v>>||>|)>=ff>||e\>v>>>>>|l,s\\e|)>\>v>>>>> + + + <\equation*> + etc\ + + + + + Pour chaque expression e> introduite dans le scope + >, on donne les deux règles suivante : + + <\equation*> + s>||>|)>=tt>||e\>v>>>>>|l\s\v|]>>,\\pre + e + + + <\equation*> + s>||>|)>=ff>>>>>|l\s\l|)>|]>>,\\pre + e + + + <\equation*> + \; + + + + + Pour toute définition apparaissant dans le scope + >, on donne la règle suivante : + + <\equation*> + s>||>|)>=tt>||e\>v>>>>>|l\sv|]>>,\\x=e + + + + + Pour tout bloc else b> + apparaissant dans le scope >, on crée deux nouveaux scopes + > et > dans lesquels on + rajoute les règles de réductions pour > et > + respectivement, et on rajoute les règles suivantes qui régissent + l'activation des deux scopes > et + > : + + <\equation*> + s>||>|)>=ff>>>>>|l\s>\ff|]>>\ff|]>> + + + <\eqnarray*> + s>||>|)>=tt>||c\>tt>>>>>|l\s>\tt|]>>\ff|]>>>||s>||>|)>=tt>||c\>ff>>>>>|l\s>\ff|]>>\tt|]>>>>>> + + + (implicitement sur toutes les règles : \activate if + c then b else b>) + + Les deux scopes > et > + héritent de la condition de reset du scope >. + + + + On se place dans le cadre \A>. On note + > l'état initial de . Les règles d'activation des + différents scopes des états se font en fonction de la variable + > définie pour l'automate comme suit : + + <\eqnarray*> + s>||r>>>>>>|l\s=s|]>>>||s>||\r>>>>>>|l\s=l|)>|]>>>>>> + + + Puis pour chaque état >, on définit > + son scope dans lequel on traduit son corps, puis on rajoute la règle + d'activation suivante : + + <\eqnarray*> + s>|||)>=s>>>>>|l\s>=tt|]>>>||s>|||)>\s>>>>>|l\s>=ff|]>>>>>> + + + Dans tous les scopes >, la condition de reset peut + être éventuellement augmentée d'un > avec une condition du + type >|)>=t>, où la variable + >> est mise à dès que l'on + emprunte une transition qui reset, et à le reste du temps. + + La règle pour une transition |c>s> + sont du style : + + <\equation*> + s>|||)>=s>||c\>tt>>>>>|l\s\s|]>> + + + À cela, il faut rajouter les conditions qui disent que l'on emprunte + exactement une transition à chaque cycle, ainsi que la partie qui définit + les variables >>. + + <\example> + On va écrire les règles de réduction qui définissent le programme suivant + : + + <\verbatim-code> + node half() returns(c: int) + + var half: bool; + + \ \ \ \ a, b: int; + + \ \ \ \ la, lb: int; + + let + + \ \ half = true -\ not pre half; + + \ \ activate + + \ \ \ \ if half then let + + \ \ \ \ \ \ \ \ a = la + 1; + + \ \ \ \ \ \ \ \ b = lb; + + \ \ \ \ tel else let + + \ \ \ \ \ \ \ \ a = la; + + \ \ \ \ \ \ \ \ b = lb + 1; + + \ \ \ \ tel + + \ \ returns a, b; + + \ \ la = 0 -\ pre a; + + \ \ lb = 0 -\ pre b; + + \ \ c = a - b; + + tel + + + Les règles de calcul des expressions sont tout le temps les mêmes. Les + règles déduites de la structure du programme sont les suivantes : + + Initialisation : + + <\eqnarray*> + s|l\s\tt|]>\ff|]>>>||s + >|||)>=tt>>>>>|l\s\tt|]>>>>>> + + + <\eqnarray*> + s + >|||)>=ff>|||)>=tt>>>>>|l\s\ff|]>>>||s + >|||)>=ff>|||)>=ff>>>>>|l\s\l|)>|]>>>>>> + + + Définition (la réduction par valeur de en + une valeur se fait selon les règles données ci-dessus) : + + <\equation*> + s>|||)>=tt>||a-b\v>>>>>|l\sv|]>> + + + Définitions de > et : + + <\equation*> + s>|||)>=tt>||pre|)> + a\v>>>>>|l\sv|]>> + + + <\equation*> + s>|||)>=tt>||pre + b|)>\v>>>>>|l\sv|]>> + + + Définition de : + + <\equation*> + s>|||)>=tt>||not + pre half|)>\v>>>>>|l\sv|]>> + + + Mémorisation des valeurs pour , et + (on écrit aussi les règles pour le cas où le scope + est inactif à titre d'exemple simplement ; en pratique celles-ci sont + éliminées puisque le scope racine est toujours actif) : + + <\eqnarray*> + s>|||)>=tt>||a\v>>>>>|l\s\v|]>>>||s>|||)>=ff>>>>>|l\s\l|)>|]>>>>>> + + + <\eqnarray*> + s>|||)>=tt>||b\v>>>>>|l\s\v|]>>>||s>|||)>=ff>>>>>|l\s\l|)>|]>>>>>> + + + <\eqnarray*> + s>|||)>=tt>||half\v>>>>>|l\s\v|]>>>||s>|||)>=ff>>>>>|l\s\l|)>|]>>>>>> + + + Activation des deux moitiés du activate : + + <\eqnarray*> + s>|||)>=tt>||half\tt>>>>>|l\s:=tt|]>\ff|]>>>||s>|||)>=tt>||half\ff>>>>>|l\s:=ff|]>\tt|]>>>>>> + + + <\equation*> + s>|||)>=ff>>>>>|l\s:=ff|]>\ff|]>> + + + Définition de et dans la première moitié : + + <\eqnarray*> + s>|||)>=tt>||la+1\v>>>>>|l\sv|]>>>||s>|||)>=tt>||lb\v>>>>>|l\sv|]>>>>>> + + + Et dans la deuxième moitié : + + <\eqnarray*> + s>|||)>=tt>||la\v>>>>>|l\sv|]>>>||s>|||)>=tt>||lb+1\v>>>>>|l\sv|]>>>>>> + + + Et c'est tout. + + + (il faudrait faire un exemple avec des automates, mais ça risque d'être + encore plus long !) + + + + On définit la traduction de en une formule + > comme suit. + + + + On utilise des formules ``à trous'' pour faire la traduction. Un trou + > correspond à la fonction e>, une formule + x=\> correspond à la fonction + a\x=e>, etc. L'argument d'une formule à trou peut + aussi être un couple d'expressions, ainsi + +\> correspond à la fonction + \e+f>. + + On définit la fonction ,e,w|)>> comme étant la + traduction de l'expression considérée dans le scope + > et devant être placée dans le trou . En pratique, + on divise en deux fonctions, une pour les expressions booléennes + et une pour les expressions numériques. Le résultat d'une traduction doit + être une formule booléenne. + + Les règles sont les suivantes : + + <\eqnarray*> + ,,e,\,e|)>,w|)>>||,e,\f.T,,\,e|)>,w,\,\,\|]>|)>|)>>>|c\\,T,c,w|)>>||>>|x\\,T,x,w|)>>|||]>>>|,pre + e,w|)>>|||)>|]>>>|,e\e,w|)>>||>|)>\T,e,w|)>|)>\s>|)>\T,e,w|)>|)>>>|,e\e,w|)>>||,,e|)>,w\\|]>|)>>>|,if + c then e else e,w|)>>||,c,\|)>\T,e,w|)>|)>\T,c,\|)>\T,e,w|)>|)>>>|,-e,w|)>>||,e,w|]>|)>>>|,\e,w|)>>||,e,w\|]>|)>>>>> + + + Par la suite, on définira la fonction de traduction d'une définition par : + + <\eqnarray*> + ,x=e|)>>||,e,s=\|)>>>>> + + + Dans le cas d'une multi-affectation ,\,x=e>, + on utilisera la traduction suivante : + + <\eqnarray*> + ,,\,x=e|)>|)>>||,e,s|)>=\\*\*\s|)>=\|)>>>>> + + + Dans le cas où l'on doit traduire une instanciation de noeud + ,\,v|)>> (c'est le cas + dans notre implémentation puisqu'on ne fait pas d'inlining), on nomme + ,\,r> les valeurs renvoyées par le noeud et + on utilise la règle ,n,\,v|)>,w|)>=w|)>,\,s|)>|]>>. + Il faut par ailleurs générer la traduction des définitions données dans le + noeud et s'occuper de passer les arguments (nommés + ,\,arg>), en introduisant des équations du + type ,v,s|)>=\|)>>. + + <\example> + Effectuons par exemple la traduction de 0 then y + else -y> : + + <\eqnarray*> + ||,if + y\0 then y else -y,s=\|)>>>|||,y\0,\|)>\T,y,s=\|)>|)>\T,y\0,\|)>\T,-y,s=\|)>|)>>>|||\0\s=s|)>\\0|)>\s=-s|)>>>>> + + + + <\example> + Effectuons la traduction de pre x + 1>. + + <\eqnarray*> + ||,0\prex + + 1,s=\|)>>>|||>|)>\T,0,s=\|)>|)>\s>|)>\T,prex + + 1,s=\|)>|)>>>|||>|)>\s=0|)>\s>|)>\T,x,1|)>,s=\+\|)>|)>>>|||>|)>\s=0|)>\s>|)>\T,1,|s=l|)>+\|)>|)>|)>>>|||>|)>\s=0|)>\s>|)>\s=l|)>+1|)>>>>> + + + Remarque : dans une étape à part, il faut penser à mémoriser une valeur + pour >, c'est-à-dire à introduire l'équation + |)>=s>. + + + + + On définit une traduction complète pour les programmes, en pensant à + introduire les équations de persistance de la mémoire pour les pre. On + introduit aussi des équations qui déterminent si un scope est actif ou + inactif, si il est init ou pas, si il doit être reset ou pas, en fonction + des divers paramètres du programme (états d'automates, conditions de blocs + activate). De manière générale, un scope a deux traductions qui sont + produites : une pour le cas où ce scope est actif, et une pour le cas où il + est inactif (dans le cas inactif, il s'agit simplement de perpétuer les + mémoires). Ainsi la traduction d'un bloc \S else b> \T sera du style + T|)>\T|)>|)>\c\T|)>\T|)>|)>>. + + Tout ceci est long à écrire, aussi nous nous contenterons de donner un + exemples. + + <\example> + Traduction du programme : + + <\verbatim-code> + node test() returns(x: int) + + var lx: int; + + let + + \ \ lx = 0 -\ pre x; + + \ \ x = if lx \= 5 then 0 else lx + 1; + + tel + + + On obtient la formule : + + <\eqnarray*> + ||>||||||)>\s|)>>>|>|l|)>\|||)>\\s|)>>>|>|l|)>\s|)>=l|)>>>>>>|)>>>>>>|)>>>||>||)>>>||>|s|)>>>||>||)>\s=0|)>\s|)>\s=l|)>|)>>>||>|\5\s=0|)>\\5\s=s+1|)>>>||>||)>=s>>>> + + + + Pour d'autres traductions, voir les sorties produites par + . + + + + Une première façon de faire un interprète pour la sémantique concrète + serait de faire un interprète de formules logiques, et d'appliquer la + formule obtenue par traduction répétitivement jusqu'à obtenir un point + fixe. + + Ce n'est cependant pas cette solution que nous avons choisi de mettre en + place, notre solution est plus proche de la sémantique par réduction. + + Nous avons choisi de représenter un état du programme en cours de + calcul comme une valeur mutables, où les variables sont calculées au fur et + à mesure qu'on les demande. La structure peut donc contenir à un + instant donné pour une certaine variable soit une valeur, soit une fonction + à appeler pour que cette valeur soit calculée et rajoutée à . + + La procédure de calcul consiste à activer le scope racine, puis à appeler + les fonctions de calcul sur les variables de sortie jusqu'à ce qu'on + obtienne des valeurs. On enregistre ensuite la portion d'état qui nous + intéresse pour le cycle suivant. + + L'activation d'un scope se fait selon la procédure suivante : + + <\itemize> + Pour une définition de variable , rajouter dans + pour la variable la fonction qui calcule et rajoute la + valeur trouvée dans . + + Pour un bloc activate, rajouter dans pour toutes les + variables renvoyées par le bloc, la fonction qui choisit la branche à + activer en calculant les conditions et active le scope correspondant. + + Pour un automate, rajouter dans pour toutes les variables + renvoyées par l'automate, la fonction qui choisit l'état à activer en se + basant sur l'état enregistré au cycle précédent, et active le scope + correspondant. + + + Le calcul de la valeur prise par une expression , utilisée dans une + condition ou pour une définition de variable, peut faire appel à d'autres + variables du programme. À ce moment si une valeur a été mémorisée on + l'utilise, sinon on appelle la fonction de calcul pour cette variable. + Lorsque le calcul d'une variable est \S en cours \T, ce statut est + enregistré dans , ce qui permet de détecter les cycles de + dépendances. + + L'étape d'enregistrement des variables d'intérêt pour le cycle suivant + comporte notamment une phase de calcul des transitions faibles empruntées + par les automates du programme, pour qu'à l'étape suivante le calcul puisse + reprendre directement. Les restart sont aussi traités à ce moment là, avec + une fonction pour reset un scope qui remet toutes les variables init à true + et tous les états à l'état initial, récursivement. + + + + Le but de l'interprétation abstraite est de prouver certaines propriétés + sur un programme. Pour cela, nous passons par une première approximation, + la sémantique collectrice, que nous approximons une seconde fois en la + passant dans un domaine de représentation abstraite. + + + + + + Notons > l'ensemble des variables. On note + > l'ensemble des variables de type énumération et + > les variables de type numérique, de sorte que + =\\\>. + + Un état du système est une fonction \\>, + où > représente l'ensemble des valeurs (numériques ou + énumération). On note =\\\> + l'ensemble des états du système. + + Avant le premier cycle, le système peut être dans n'importe quel état de + : + + <\eqnarray*> + ||\ + \| s|)>=tt|}>>>>> + + + Entre deux cycles, les variables qui comptent réellement dans sont + les variables actif et reset pour les scopes, les variables d'état pour les + automates, et les mémoires des . + + Vision habituelle : on a une suite d'états + ,s,\> qui représentent la mémoire entre deux + cycles. > est défini. On a une relation de transition qui + prend > et les entrées > et qui calcule les + sorties > et l'état suivant > : + + <\equation*> + s|i>o,s|i>o,s|i>o,s\*\* + + + Nous introduisons ici une seconde notation pour ce fonctionnement. + + Les variables de l'état précédent >, au lieu d'être + considérées comme un lieu à part, sont partiellement copiées dans l'état + > par une fonction que l'on appellera fonction de cycle. + Cette fonction copie uniquement les variables dont les valeurs précédentes + sont utiles pour le calcul de la transition, et préfixe leur noms d'un + préfixe standard, \S \T, qui indique que ce sont des variables de + type , c'est-à-dire des copies de valeurs du cycle précédent. + + On note cette fonction de cycle \\|)>> ; nous écrivons + cette fonction comme non-déterministe car après cette fonction un certain + nombre de variables sont oubliées et on considère que leurs valeurs n'ont + pas d'importance. Elle peut être définie à partir d'un ensembles de + variables , qui sont les variables qui nous intéresseront lors du + calcul de la transition : + + <\eqnarray*> + >||\\ + \| \x\C,s=s|}>>>>> + + + Déroulement d'un cycle : on prend l'état après passage par la + fonction de cycle, on y met les valeurs des entrées du système. On applique + ensuite la fonction \\> qui calcule + toutes les variables du système (elle peut être définie comme la saturation + de la sémantique par réduction, comme le point fixe de l'application + répétée d'une formule, ou plus classiquement comme l'application d'une + série d'instructions en style impératif, résultat de la compilation du + programme). On peut à ce moment récupérer les valeurs de sorties. + + Avec nos notations : > est la restriction de + |)>+i|)>> aux variables de + sortie, où |)>+i> correspond à définir + les variables de |)>> et de >. + + <\remark> + En principe, quel que soit c|)>>, + |)>> ne peut être qu'un seul + environnement, car le programme est déterministe. C'est pourquoi on se + permet l'abus de notation |)>+i|)>>. + + + + + On s'intéresse maintenant à l'exécution d'un programme SCADE quelles que + soient ses entrées >. On peut faire des hypothèses sur ces + entrées en utilisant la directive du langage. On suppose + que l'on dispose d'une fonction \> qui nous dit si un + environnement est conforme à la spécification donnée par les directives + . + + On s'intéresse maintenant à la sémantique non déterministe suivante : + + <\eqnarray*> + >||\ + \| s|)>=tt|}>>>|>|||)>>>|>||x>,a\c,q|)>=tt|}>>>>> + + + \; + + La valeur > contient tous les environnements possibles pour + le système à la -ème étape, quelles que soient les entrées jusque + là. + + On définit maintenant la sémantique collectrice du programme comme étant la + valeur : + + <\eqnarray*> + ||> + s.s\g|)>>>||>||)>>>>> + + + représente ici exactement l'ensemble de tous les états accessibles + par le système, à tout moment, quelles que soient les valeurs en entrée. + + Toute la suite de notre travail consistera à construire une approximation + la meilleure possible de . + + + + Une abstraction est définie par une correspondance de Galois entre + |)>> et >, + représentation abstraite d'une partie de >. L'abstraction + peut être caractérisée par sa fonction de concrétisation : + + <\eqnarray*> + >>||\\|)>>>>> + + + \ On peut aussi généralement s'appuyer sur l'existence d'une + fonction d'abstraction : + + <\eqnarray*> + >>|||)>\\>>>> + + + Cette fonction fait correspondre à une partie de > sa + meilleure approximation dans le domaine abstrait (par exemple dans le cas + des polyèdres, l'abstraction d'un ensemble fini de points est leur + enveloppe convexe, mais un cercle n'a pas de meilleure abstraction). + + Dans tous les cas, on s'attend à ce que + x\\,x\\|)>> + d'une part et y\\|)>,y\\|)>> + d'autre part. + + De base ici, nous avons deux choix simples pour > : + les intervalles et les polyèdres convexes. Ceux-ci sont considérés acquis + pour la suite ; on les note > et + >, avec les fonctions de concrétisation + > et > associées. + + On note > l'ensemble des équations (égalités et inégalités) + sur des variables de >. Par exemple les éléments suivants + sont des équations de > : + 5*x-2>. + + Pour \> et \>, on note + e> si l'expression est vraie dans l'état . + + Pour un domaine abstrait > et pour une expression + \>, on suppose que l'on a une fonction sémantique + |e|\> : + \\\> qui restreint + l'abstraction > en une sur-approximation (la meilleure + possible) de \|)> + \| s\e|}>|)>> : + + <\eqnarray*> + \|)> + \| s\e|}>>|>||e|\>|)>|)>>>>> + + + La fonction de transition est représentée dans l'abstrait par une + fonction > qui correspond à l'application d'un certain + nombre de contraintes de >, ainsi que de disjonction de cas. + On remarque que l'aspect impératif disparaît complètement, on n'a plus + qu'un ensemble d'équations et de disjonctions. La traduction du programme + SCADE en formule logique donne directement une formule de ce style que l'on + peut appliquer sur un environnement abstrait. + + La fonction de cycle correspond à conserver un certain nombre de + variables en tant que \S mémoires \T, en préfixant leur noms d'un \S L \T + pour . Notons l'ensemble des variables à conserver. Cette + fonction peut être représentée dans l'abstrait par l'opérateur + > dont une définition est : + + <\eqnarray*> + >||\\ + \| \x\C,\\\\\|\=\|}>|)>>>>> + + + (cette définition n'est pas constructive car on n'implémente jamais + > directement) + + Cela correspond à oublier un certain nombre de variables qui ne nous + intéressent plus, et à renommer celles que l'on garde. + + <\example> + Soit le programme suivant : + + <\verbatim> + node counter() returns(x: int) + + \ \ x = 0 -\ (if pre x = 5 then 0 else pre x + 1) + + + Celui-ci est traduit par une formule du style : + + <\eqnarray*> + ||\Lnreset>>||>|\ff>>||>||\tt\x=0|)>>>|>|\ff\|x=0|)>>>|>|5\x=Lx+1|)>>>>>>|)>|)>>>>>>|)>>>>> + + + Les deux variables qui ont besoin d'être perpétuées d'un cycle au suivant + sont > et , la fonction de cycle + > est donc définie à partir de + ,x|}>>. + + La fonction >, quant à elle, reflète directement la + structure de la formule : + + <\eqnarray*> + >|||init\Lnreset|\>\|nreset\ff|\>||init\tt|\>\|x=0|\>>>|>||init\ff|\>||Lx=5|\>\|x=0|\>>>|>||Lx\5|\>\|x=Lx+1|\>>>>>>|)>>>>>>|)>>>>> + + + + Par facilité, on note =c\f>. Étant + donné qu'un programme est essentiellement une grosse boucle, la valeur qui + nous intéresse est l'abstraction de donnée par : + + <\eqnarray*> + >||>i.I\g|)>>>>> + + + Où > est l'état initial du système et est défini par + =|i|\>|)>>, + où est une équation du type =tt>. + + Nous en venons donc à chercher des domaines abstraits les mieux à même de + représenter les différentes contraintes exprimables dans >. + Dans notre cas, celles-ci se divisent essentiellement en deux catégories : + + <\itemize> + Contraintes numériques : les variables sont dans + >, les constantes dans > (ou + >), les opérateurs sont ,\, + mod,=,\,\>. On note > l'ensemble + de telles contraintes. + + Contraintes énumérées : les variables sont dans + >, les constantes dans un ensemble fini qui dépend + du types des variables, les opérateurs sont ,\>. + On note > l'ensemble de telles contraintes. + + + Les domaines numériques > et + > ne sont pas à même de représenter + correctement les contraintes de >. Généralement, on + définit : + + <\eqnarray*> + e\\\,|e|\>>||>>>|e\\,|e|\>>||>>>>> + + + Les variables booléennes peuvent être représentées par et + , par exemple on peut introduire les transformations suivantes (en + notant > l'ensemble des variables à valeurs + booléennes) : + + <\eqnarray*> + x\\,|x=tt|\>>|||x=1|\>>>|x\\,|x=ff|\>>|||x=0|\>>>|x,y\\,|x=y|\>>|||x=y|\>>>|x,y\\,|x\y|\>>|||x=1-y|\>>>>> + + + Les résultats sont généralement plus que médiocres. De plus, on ne peut pas + représenter ainsi de façon exacte les valeurs d'énumérations ayant plus de + deux éléments (puisqu'on se restreint à une enveloppe convexe). + + + + Pour l'analyse de programmes SCADE, l'analyse de l'ensemble de la boucle de + contrôle comme une seule valeur dans un environnement abstrait numérique + est insuffisante. Il nous a donc été crucial de développer des domaines + abstraits capables de faire des disjonctions de cas afin de traiter de + manière plus fine l'évolution du programme. + + Nous souhaitons pouvoir faire des disjonctions de cas selon les valeurs des + variables de >. Par exemple si on a un automate + dont la variable d'état s'appelle et évolue dans + l'ensemble >, on voudrait + pouvoir isoler cette variable des autres, ne plus l'inclure dans le domaine + abstrait et l'utiliser pour différencier plusieurs valeurs abstraites. Il + nous faut donc redéfinir le domaine abstrait > et surtout la + fonction d'application d'une condition |e|\>> + avec \>. + + + + Supposons que l'on ait maintenant trois ensembles de variables : + + <\itemize> + > : variables numériques + + > : variables énumérées non considérées + comme variables de disjonction + + > : variables de disjonction, prenant leurs + valeurs dans > un ensemble fini (pour être précis, + il faudrait noter x\\>, + > l'ensemble des valeurs possibles + pour la valeur , qui peut être différent selon la variable - on + est amené à faire un peu de typage, il faut en particulier s'assurer que + les contraintes que l'on donne sont entre deux variables pouvant prendre + les mêmes valeurs). + + + On considère dans cette section que l'on a un domaine abstrait + > capable de gérer les contraintes sur les + variables numériques et sur les variables énumérées, mais sans relation + entre les deux. Le domaine > représente une + abstraction de =\\|)>\\>. + On note > et > les éléments + bottom et top de ce treillis, > et + > les bornes inf et sup de ce treillis, ainsi que + > son opérateur de widening. On note + |\|\>> la fonction + de restriction par une contrainte. + + La particularité des variables de disjonction est que l'on ne réalise pas + d'abstraction sur celles-ci : on représente directement un état par une + valuation de ces variables, dans \\=\>. + + On appelle toujours =\\\>, où + =\\\\\>. + On a une injection évidente de > dans + |)>>, on identifie donc + \> à \\|\x\\,s=d|}>>. + De même on identifie \> à + \ \| \x\\\\,s=e|}>>. + + On construit maintenant le domaine abstrait disjonctif comme suit : + + <\eqnarray*> + >||\\>>|>||\>d\\|)>>>>> + + + Les éléments > et > sont définis comme suit : + + <\eqnarray*> + >||d.\>>|>||d.\>>>> + + + On vérifie bien que |)>=\> et + |)>=\>. + + On peut aussi définir les opérations > et > : + + <\eqnarray*> + t>||d.\t|)>>>|t>||d.\t|)>>>>> + + + Enfin, la partie intéressante : on peut définir un certain nombres + d'opérateurs de restriction : + + <\itemize> + x,y\\,\s\\>, + + <\eqnarray*> + |x=y|\>>||d.>|=d>>|>|>>>>>>||x\y|\>>||d.>|\d>>|>|>>>>>>>> + + + x\\,\v\\>, + + <\eqnarray*> + |x=v|\>>||d.>|=v>>|>|>>>>>>||x\v|\>>||d.>|\v>>|>|>>>>>>>> + + + + |e|\>> est donc défini correctement + pour tout \>, où > est + l'ensemble des conditions sur variables de disjonction de + >. Pour toute expression + \> ou \>, le + domaine > est sensé savoir les prendre en + compte de manière satisfaisante, on définit donc : + + <\eqnarray*> + e\\\\,|e|\>>||d.|e|\>|)>>>>> + + + L'opérateur de widening reste problématique. On peut définir un opérateur + de widening point par point : + + <\eqnarray*> + + t>||d.s \ + t>>>> + + + Mais celui-ci est peu satisfaisant car chaque état + \> représente potentiellement un état d'un + système de transitions, pouvant déboucher sur lui-même ou sur un autre + état, et il faut savoir prendre en compte ces disjonctions à un niveau plus + fin. Il faut donc plutôt voir le tout comme un système de transitions. + + Étant donné notre système représenté par une fonction de transition + > et une fonction de cycle > (par facilité, + on notera =c\f>), l'ensemble des + états accessible par le système est =lfp>s.I\g|)>>, + où =|i|\>|)>>. + + Pour \\>, notons + > : \\\> + tel que >=\d.>|d>>|>|>>>>>> + + Le principe des itérations chaotiques peut s'écrire comme suit : + + <\itemize> + Poser : + + <\eqnarray*> + >||>>|>||\\| + s\\|}>>>>> + + + Tant que \\>, on répète + le processus suivant : + + <\eqnarray*> + >|>| + >>|>||>|)>|)>>>|>||\D>>|>||\\|}>|)>\\\|s\s|}>>>>> + + + + Intuitivement : > représente l'ensemble des états + possibles pour notre système de transition. À chaque itération, on choisit + un état qui a grossi depuis la dernière fois. On calcule ses successeurs et + on met à jour l'ensemble des états que l'on connaît. + + Problème : ici on ne fait pas de widening, et on peut être à peu près sûr + que l'analyse ne terminera pas (sauf cas simples). Pour cela, on introduit + un ensemble >\\> qui + représente l'ensemble des états que l'on devra faire grossir par widening + et non par union simple dans le futur. La définition devient alors : + + <\eqnarray*> + >||>>|>||\\| + s\\|}>>>|,0>>||>>>> + + + <\eqnarray*> + >|>| + >>|>||>|)>|)>>>|>||d. + \ D>|K,n>>>| + \ D>|>>>>>>|,n+1>>||,n>\\\| + s\\\s\s|}>>>|>||\\|}>|)>\\\|s\s|}>>>>> + + + Ie : si un état est apparu à une étape, et si à une étape ultérieure il + grossit, alors lors de toutes les étapes suivantes on le fera grossir non + pas par union simple mais par élargissement. + + Reste une question : comment prendre en compte les conditions de boucle qui + permettent de réduire le domaine abstrait ? La définition précédente n'est + peut-être pas la bonne, car elle risque d'appliquer des élargissements que + l'on ne sait plus ensuite comment rétrécir pour refaire apparaître les + bonnes conditions. Nous proposons comme forme final le processus + d'itération suivant : + + <\eqnarray*> + >||>>|>||\\| + s\\|}>>>|,0>>||>>>> + + + <\eqnarray*> + >|>| + >>|>||>|)>>i.r>\g|)>|)>>>|>||\g|)>>>|>||d. + \ D>|K,n> et d\a>>| + \ D>|>>>>>>|,n+1>>||,n>\\\| + s\\\s\s|}>>>|>||\\|}>|)>\\\|s\s|}>>>>> + + + Où le point fixe > est calculé avec appel au + widening au besoin, et en faisant une ou des itérations décroissantes à la + fin. Intuitivement : on fait grossir un état au maximum, en cherchant son + point fixe en boucle sur lui-même. Ensuite seulement on s'occupe de savoir + ce qu'il peut propager aux autres états. + + + + Nous proposons dans ce paragraphe un second domaine abstrait capable de + faire des disjonctions de cas, et qui permet de mieux traîter des problèmes + ayant un nombre important de variables de type énuméré reliées entre elles + par des relations complexes. + + Définition du domaines abstraits avec graphes de décision : on va écrire + ici une définition mathématique des opérateurs que l'on a implémenté. On + fait abstraction des problématiques de mémoisation et de partage des + sous-graphes, qui font tout l'intérêt de la technique d'un point de vue + pratique mais qui peuvent être considérés comme un traitement à part (ce + n'est rien de plus que de la mémoisation et du partage). + + + + Il y a deux domaines de variables, > pour les + énumérés et > pour les variables numériques. Il y a + deux domaines pour les contraintes, > les + contraintes sur les énumérés (de la forme y> ou + v,v\\>) et > + les contraintes sur les variables numériques (égalités ou inégalités). + + + + On note > le domaine des valeurs numériques et + >, >, + |\|\>>, + >, >, + >, >, + > les éléments correspondants dans ce domaine. On + considère que : + D\\|)>> (avec + =\\\\\>) + donne toutes les valuations possibles pour les variables de + >. + + + + On définit un ordre sur les variables de > : + =,x,\,x|}>> + (bien choisi pour réduire la taille du graphe). + + On définit ensuite une valeur du domaine disjonctif, ie un EDD, par un type + somme comme suit : + + <\eqnarray*> + |>|D|)>>>|||,v\s,v\s,\,v\s|)>>>>> + + + Si on voit ça comme un arbre, alors il faut que si un noeud + ,\|)>> est ancêtre d'un noeud + ,\|)>>, alors j> (par + rapport à l'ordre donné sur >).\ + + Pour faciliter les notations, on introduit le rang d'un noeud : + + <\eqnarray*> + ,v\s,\,v\s|)>|)>>||>||)>>||>>>> + + + La contrainte se traduit par, pour tout noeud + ,v\s,\,v\s|)>>, + on a j,i\\|)>>. + + On définit aussi la contrainte suivante : on n'a pas le droit d'avoir de + noeud ,v\s,v\s,\,v\s|)>> + si =s=*\*=s>. Cela implique + l'unicité de l'arbre qui représente un environnement donné. + + La concrétisation est définie comme suit : + + <\eqnarray*> + |)>>||>>|,v\s,\,v\s|)>|)>>||\|)> + \| s|)>=v|}>>>>> + + + Les éléments > et > sont définis comme suit : + + <\eqnarray*> + >|||)>>>|>|||)>>>>> + + + Pour assurer l'unicité lors des transformations, on définit la fonction de + réduction : + + <\eqnarray*> + |x,v\s,\,v\s|)>|\>>||>|=s=*\*s>>|,v\s,\,v\s|)>>|>>>>>>>> + + + L'opération > est définie comme suit : + + <\eqnarray*> + \V|)>>||t|)>>>||,v\s,\,v\s|)>>>|>|,v\s,\,v\s|)>>>>>>>||,v\s\s,\,v\s\s|)>>>|,v\s,\,v\s|)>\s>|\|)>>>>>||x,\s\s>>|>>|\s\s>>>>>|)>|\>>>>>>>>>> + + + et symétriquement lorsque \\|)>> + (le noeud le plus haut est celui correspondant à la variable d'indice le + plus faible, pour respecter l'ordre). + + L'opération > est définie pareil. + + Si \>, on définit + |e|\>> par : + + <\eqnarray*> + |e|\>|)>>|||e|\>|)>>>||e|\>,v\s,\,v\s|)>|)>>||,v\|e|\>|)>,\,v\|e|\>|)>|)>>>>> + + + Pour les conditions sur les énumérés, on définit d'abord : + + <\eqnarray*> + v|)>>||\,v\\,v\\\\|)>>>|v|)>>||\,v\\,v\\\\|)>>>|\x|)>>|j>>|,v\c\v|)>,\,v\c\v|)>|)>>>|\x|)>>|j>>|,v\c\v|)>,\,v\c\v|)>|)>>>>> + + + et symétriquement lorsque i>. + + On peut ensuite poser, pour \> : + + <\eqnarray*> + |e|\>>||\s>>>> + + + L'égalité entre les valeurs représentées par deux EDD correspond à + l'égalité de ces deux EDD (c'est une CNS). + + L'inclusion est également définie par induction : + + <\eqnarray*> + \V|)>>|>|t>>|,v\s,\,v\s|)>\C,v\s,\,v\s|)>>|>|s\s>>|C,v\s,v\s,\,v\s|)>>||lorsque + \\i>>|s\s>>|,v\s,v\s,\,v\s|)>\s>||lorsque + i\\|)>>>|s\s>>>> + + + + + Sur nos EDD, on définit une opération :D\D\D> + comme suit : + + <\eqnarray*> + ,V|)>>||>|>>|>|>>>>>>|,C,v\s,\,v\s|)>|)>>||,v\\,s|)>,\,v\\,s|)>|)>>>>> + + + Explication : cette fonction extrait d'un EDD la fonction booléenne qui + mène vers exactement une certaine valeur abstraite des numériques. + + On introduit maintenant un opérateur de widening sur nos arbres : + + <\eqnarray*> + b>||>>>|>,V|)>|)>>|| t|)>>|=\,b|)>>>|t|)>>|>>>>>>|>,v\s,\,v\s|)>|)>>|\>>|,\f>|)>>>|>>|\f>|)>>>>>>|)>>>>> + + + Les autres cas sont définis exactement pareil (cf définition de + >, plus on passe et à notre fonction + >>). Explication : lorsque l'on doit faire l'union de + deux feuilles, on fait un widening si et seulement si les deux feuilles + sont accessibles selon exactement la même formule booléenne sur les + énumérés dans et . + + > + + On enrichit un peu notre arbre au niveau des feuilles pour enregistrer + quelques informations supplémentaires : + + <\eqnarray*> + |>|>>|||>>>|||,v\s,v\s,\,v\s|)>>>>> + + + L'étoile correspondra à : \S cette feuille est nouvelle, il faut l'analyse + comme nouveau cas \T, et l'indice \> correspond à : \S + cette feuille est là depuis itérations \T, où le permet + d'implémenter un délai de widening. + + On se donne > un délai de widening, paramètre de l'analyse. On + définit maintenant une fonction d'accumulation > comme + suit : + + <\eqnarray*> + + b>||>>>|>,V|)>>|\>>|>>|>>,\|)>>||>>>|>>,V|)>|)>>|| t|)>>>|=\,b|)> + i\\>>|t|)>>>|>>>>>>|>,v\s,\,v\s|)>|)>>|\i>>|,\f>|)>>>|>>|\f>|)>>>>>>|)>>>>> + + + (où > correspond à soit une étoile soit pas d'étoile) + + (les autres cas se font par appel récursif encore une fois comme dans le + cas de l'union) + + Puis une fonction de détection des cas nouveaux par rapport à une valeur + précédente : + + <\eqnarray*> + >>||>,s,s|)>>>|>,s,V|)>>||>>|\s|)>\s>>|>|>>>>>>|>,s,V>|)>>||>>>|>,s,C,v\s,\,v\s|)>|)>>||,v\f>,s,s|)>,\,v\f>,s,s|)>|)>>>>> + + + Nous sommes maintenant en mesure de décrire le processus d'itérations + chaotiques à proprement parler. On commence avec : + + <\eqnarray*> + >||> + I>>>> + + + (appliquer > de la sorte permet de faire que toutes les + feuilles soient étoilées) + + Puis pour les itérations, deux cas : + + <\itemize> + Si il existe |)>>> + une feuille étoilée dans > : on marque + > l'arbre > où toutes les + feuilles |)>> sont dé-étoilées, puis : + + <\eqnarray*> + >||,s|)>>>|>||\s>i.c\\g|)>|)>>>|>||\g|)>>>|>||> + \ D|)>>>>> + + + (où le point fixe > est fait en faisant appel à + > et > définis précédemment, avec un délai + de widening convenable) + + Dans tous les cas, on refait une itération. Les étoiles finiront bien par + disparaître. + + Si il n'existe pas de telle feuille étoilée dans > : + + <\eqnarray*> + >||> + \ g|)>|)>>>>> + + + Dans ce cas, on s'arrête si =s>. + + + + + Une autre approche à base de partitionnement dynamique a été tentée, mais + elle n'a pas donné de très bons résultats par manque d'une heuristique sur + les partitionnements à effectuer. Détails à venir. + + + + Le projet scade-analyzer propose une implémentation simple des composants + suivants : + + <\itemize> + parser, lexer, typeur pour notre sous-ensemble de SCADE (source des + fichiers dans ) + + interprète pour la sémantique cocnrète + () + + implémentation de la transformation d'un programme en formule + logique ; quelques simplifications sur les formules logiques + (, ). + + domaine numérique non-relationnel basé sur les intervalles ; + domaine relationnel basé sur la bibliothèque externe Apron + (, , + , ...) + + deux domaines abstraits et analyseur statique correspondant + (, ) + + + En nous basant sur les options de la ligne de commande, nous allons + maintenant décrire les différentes fonctionnalités. + + + + <\itemize> + : parse un fichier SCADE et le ré-affiche en + sortie + + : parse un fichier SCADE et le ré-affiche en + sortie, après une étape de renommage qui consiste à rendre les noms + unique au sein d'un noeud. Cette passe est implémentée dans + . + + + + + <\itemize> + : execute le programme SCADE donné en argument, + avec l'interprète basé sur la + sémantique à réduction. Le programme doit satisfaire la spécification + suivante : avoir un noeud qui servira de racine, ce noeud + devant prendre une unique entrée, , qui est un compteur + incrémenté à chaque cycle, et renvoyant trois entiers, , + et (qui seront affichés en sortie), ainsi qu'un + booleen qui indiquera que l'interprète doit terminer. Cf + fichiers dans pour des exemples. + + : pareil mais affiche plus de détails (tout le + contenu de la mémoire est affiché à chaque cycle). + + + + + + + Cette analyse est implémentée dans . + + + + <\itemize> + : fait une passe d'analyse statique par + interprétation abstraite utilisant le domaine à disjonctions simples, et + en s'appuyant sur le domaine non-relationnel à base d'intervalles pour la + partie numérique + + : de même mais utilise le domaine abstrait + relationnel basé sur Apron (polyèdres) pour la partie numérique + + + + + <\itemize> + noeud\> : spécifie le noeud racine + dont on veut faire l'analyse (par défaut : ) + + : affiche des détails sur le contenu de + l'accumulateur à chaque itération + + : affiche encore plus de détails + + n\> : définit un délai pour les + opérations de widening (par défaut 5) + + vars\> : variables à utiliser comme + variables de disjonction (par défaut : aucune) + + scopes\> : donne un certain + nombre de scopes pour lesquels ne pas introduire de variable + (par défaut , c'est-à-dire que + n'est jamais introduite). Lorsqu'une variable + est introduite, on génère les équations qui font en sorte + que soit égal au numéro du cycle depuis le début de + l'exécution du programme. + + scopes\> : donne un certain nombre + de scopes pour lesquels introduire une variable (par + défaut ). Il est envisageable de remplacer la variable + de chaque scope par une variable , les + disjonctions de cas init/non init se feront alors selon la condition + ou 1>. En ne générant ni variable + ni variable , la disjonction n'est pas + faite. + + + + + Cette analyse est implémentée dans . + + + + <\itemize> + : fait une passe d'analyse statique + utilisant le domaine à base d'EDD et en utilisant les intervalles comme + domaine de valeurs numériques + + : de même mais utilise le domaine abstrait + relationnel basé sur Apron (polyèdres) pour la partie numérique + + + + + <\itemize> + + + , + + + + , + + Non implémenté : paramètre pouvant intervenir sur + le choix des variables à considérer dans le graphe de décision + (actuellement toutes sont nécessairement considérées). + + + + + Une troisième forme d'analyse, basée sur un partitionnement dynamique de + > a été tentée. Celle-ci n'a pas donné de très bons + résultats, mais nous indiquons néanmoins son existence ici. + L'implémentation existe dans . + + + + <\itemize> + : analyse par partitionnement dynamique, + utilise un domaine simple non-relationnel pour les valeurs énumérées et + les intervalles pour la partie numérique + + : analyse par partitionnement dynamique, + utilise des graphes de décision pour représenter les conditions sur les + énumérées et les intervalles pour la partie numérique + + + + + + + + + <\itemize> + + + + + , + + , + + : profondeur maximale de + partitionnement + + : largeur maximale de partitionnement + (ie nombre maximal de parties à considérer) + + + + + + + <\itemize> + Implémenter un domaine d'intervalles permettant de gérer les + rationnels en précision arbitraire, ou se brancher sur le module Box + d'Apron + + Utiliser un opérateur de widening aproprié (cf Astrée) + + Implémenter la sémantique des nombres flottants machine (ce qui + n'est pas simple) + + + + + <\itemize> + Modification du domaine EDD pour pouvoir ne prendre en compte + qu'une partie des variables énumérées (pour l'instant elles sont toutes + considérées, ce n'est pas paramétrable). Permettre que les feuilles + contiennent également des informations non-relationnelles sur les + variables de type énuméré. + + Analyse de base avec des intervalles, plus des \S packs \T de + variables traités avec des domaines plus puissants (octagones, + polyhèdres, domaines à disjonctions) + + Analyse par contrats : abstraire certains noeuds par les garanties + que vérifient les sorties, plutôt que de considérer le noeud en entrée. + En échange, il faut que l'on vérifie que les propriétés en entrée + (assume) sont bien vraies. + + L'ordre des équations dans le programme semble avoir un impact sur + l'analyse : si celles-ci sont écrites dans l'ordre où elles seront + effectivement exécutées (ie triées par ordre de dépendance), l'analyse + semble gagner en précision. Implémenter une passe de scheduling + (approximatif : on ne veut pas diviser les automates, les blocs activate, + ...) que l'on exécuterait comme pré-processing sur le programme. + + + + + <\itemize> + , , International Symposium on Static Analysis, SAS'94. + + , and , + , IEEE Transactions on + Software Engineering, Spcial Issue on the Specification and Analysis of + Real-Time Systems, Sept. 1992 + + , and , + , Static + Analysis Symposium, SAS'99. + + + \; + + +<\initial> + <\collection> + + + + +<\references> + <\collection> + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + + + +<\auxiliary> + <\collection> + <\associate|toc> + |math-font-series||1Introduction> + |.>>>>|> + + + |math-font-series||2Spécification> + |.>>>>|> + + + |2.1Grammaire + |.>>>>|> + > + + |2.2Sémantique concrète + |.>>>>|> + > + + |2.3Sémantique par réduction + |.>>>>|> + > + + |2.3.1Règles de réduction pour + l'activation du scope racine |.>>>>|> + > + + |2.3.2Règles de réduction pour + l'init dans tous les scopes |.>>>>|> + > + + |2.3.3Règles de réduction + d'expressions |.>>>>|> + > + + |2.3.4Règles de réduction pour + les pre |.>>>>|> + > + + |2.3.5Règles de réduction pour + les définitions de variables |.>>>>|> + > + + |2.3.6Règles de réduction pour + les blocs activate |.>>>>|> + > + + |2.3.7Règles de réduction pour + les automates |.>>>>|> + > + + |2.4Sémantique par traduction, + règles de traduction |.>>>>|> + > + + |2.4.1Traduction des expressions + numériques et booléennes |.>>>>|> + > + + |2.4.2Traduction de scopes et de + programmes |.>>>>|> + > + + |math-font-series||3Interprète + pour sémantique concrète> |.>>>>|> + + + |math-font-series||4Interprétation + abstraite> |.>>>>|> + + + |4.1Sémantique collectrice + |.>>>>|> + > + + |4.1.1Nouvelle notation : + fonction de transition |.>>>>|> + > + + |4.1.2Suppression des entrées, + sémantique collectrice |.>>>>|> + > + + |4.2Généralités sur + l'interprétation abstraite |.>>>>|> + > + + |math-font-series||5Domaines + abstraits et disjonction de cas> |.>>>>|> + + + |5.1Domaine à disjonction + simple |.>>>>|> + > + + |5.2Domaine à graphe de + décision |.>>>>|> + > + + |5.2.1Variables et contraintes + |.>>>>|> + > + + |5.2.2Domaine numérique + |.>>>>|> + > + + |5.2.3Les EDD + |.>>>>|> + > + + |5.2.4Opérateur de widening + |.>>>>|> + > + + |5.2.5>.>>>>>>>|Itérations + chaotiques. |.>>>>|> + >>|font-series||Itérations + chaotiques.> |.>>>>|> + > + + |Itérations chaotiques. + |.>>>>|> + > + + |math-font-series||6Implémentation> + |.>>>>|> + + + |6.1Parsing et affichage de + programmes SCADE |.>>>>|> + > + + |6.2Interprète SCADE + |.>>>>|> + > + + |6.3Analyse statique par + interprétation abstraite |.>>>>|> + > + + |6.3.1Domaine à disjonctions + simples |.>>>>|> + > + + |Modes d'analyse + |.>>>>|> + > + + |Options de l'analyse + |.>>>>|> + > + + |6.3.2Domaine à disjonction par + graphe de décision |.>>>>|> + > + + |Modes d'analyse + |.>>>>|> + > + + |Options de l'analyse + |.>>>>|> + > + + |6.3.3Analyse par partitionnement + dynamique |.>>>>|> + > + + |Modes d'analyse + |.>>>>|> + > + + |Paramètres de l'analyse + |.>>>>|> + > + + |math-font-series||Bibliographie> + |.>>>>|> + + + + \ No newline at end of file -- cgit v1.2.3