summaryrefslogtreecommitdiffstats
path: root/doc/soutenance/soutenance.tex
blob: 1d57e21e08480dbc1a227cb07659649105d5f2b7 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383

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