\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}

\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}
\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}
\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}

\begin{frame}
\titlepage
\end{frame}

\begin{frame}\frametitle{Introduction}
  \begin{itemize}
  	\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}

\begin{frame}
\frametitle{Plan}
\tableofcontents
\end{frame}

% ----------------------
% contenu

\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}$~: ensemble des variables
    \item $\mathbb{V}$~: ensemble des valeurs
  \end{itemize}
  Ce modèle simple suffit !
  \begin{definition}
    Environnement mémoire~: fonction de $\mathbb{X}\to\mathbb{V} = \mathbb{M}$
  \end{definition}
\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$$
  Autre écriture~:
  $$s_n = f(c(s_{n-1}) + i_n)$$
\end{frame}
\begin{frame}\frametitle{Sémantique collectrice}
	\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}
  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}
	\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}
    \centering
    \def\svgwidth{.9\textwidth}
    \input{alpha-gamma.pdf_tex}
  \end{figure}
\end{frame}
\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}
	\begin{itemize}
	  \item On abstrait $S$ par $S^\sharp$ tel que $S \subset \gamma(S^\sharp)$.

	  \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}
    \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 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}
\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{Disjonctions de cas selon des variables}
	\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~:
  \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{Principe d'itération}
  On construit $S^\sharp$ incrémentalement.
  \begin{itemize}
    \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}
  \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 est souvent confronté à des représentations comme celle-ci~:
  \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}
	\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~:
  \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{Principe d'itération}
	\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{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~: 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{Résultats}
	Quelques programmes sur lesquels j'ai pu prouver des propriétés intéressantes~:
  \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{Références}
  \bibliographystyle{apacite}
  \bibliography{research}
\end{frame}


\end{document}