main.tex

   1 \documentclass[11pt,a4paper]{article}
   2
   3 \usepackage[latin1]{inputenc}
   4 \usepackage[T1]{fontenc}
   5 \usepackage{lscape}
   6 \usepackage{fullpage}
   7
   8
   9 \usepackage{tikz}
  10 \usetikzlibrary{shapes}
  11 \usetikzlibrary{fit}
  12 \usetikzlibrary{matrix}
  13
  14 \newcommand{\eg}{par exemple}
  15
  16 \title{Analyse statique de modèles Matlab/Simulink~:\\
  17   vers une plate-forme logicielle coopérative}
  18
  19 \author {A.C., O.B. et S.Z.}
  20
  21 \date{\today}
  22
  23 \begin{document}
  24
  25 \maketitle
  26
  27 \section{Contexte}
  28 \label{sec:contexte}
  29
  30 La conception de systèmes embarqués de contrôle-commande nécessite une
  31 phase de modélisation et de simulation de processus physiques
  32 complexes avant la mise en {\oe}uvre. Cette phase est généralement
  33 réalisée à l'aide d'outils de conception tels que Matlab/Simulink et
  34 suit le modèle dit de la conception fondée sur la simulation, très
  35 utilisée en automobile notamment. Ce modèle s'appuie sur deux grandes
  36 étapes nommées~:
  37 \begin{itemize}
  38 \item Model in The Loop (MTL)~: étape permettant de définir les lois de
  39   commande de manière haut niveau en prenant en compte un modèle du
  40   processus physique à commander. La loi de commande est définie dans le
  41   même formalisme que le processus physique (généralement des plances
  42   Simulink). La simulation numérique permet de
  43   vérifier/tester que la loi de commande correspond aux attentes.
  44 \item Software in The Loop (STL)~: étape vérifiant par simulation
  45   numérique que l'implémenta\-tion de la loi de commande, \eg{} en
  46   langage C, correspond toujours aux attentes. A ce niveau,
  47   l'implémentation de la loi de commande interagit avec le modèle du
  48   processus physiques: les deux sont décrits dans des formalismes
  49   différents.
  50 \end{itemize}
  51
  52
  53 L'analyse statique par interprétation abstraite est une méthode de
  54 vérification formelle qui permet de prouver des propriétés sur les
  55 programmes informatiques. Pour prouver ces propriétés, l'analyse
  56 statique va généralement essayer de calculer des \emph{invariants} sur
  57 le programme (i.e.  une formule logique qui doit être vraie pour toutes
  58 les exécutions du programme) en effectuant une \emph{abstraction} du
  59 processus physique, par exemple en ne gardant que les ranges de valeurs
  60 admissibles pour chaque grandeur physique. Dans ce projet, nous nous
  61 intéressons particulièrement aux invariants numériques, c'est-à-dire des
  62 invariants dont les formules logiques portent sur les valeurs associées
  63 aux variables du programme. Le but de ce projet est l'application de ces
  64 techniques sur les modèles Matlab/Simulink utilisés dans la phase MTL~:
  65 ainsi, des erreurs de conception de la loi de contrôle-commande peuvent
  66 être détectées au plus tôt dans le cycle de développement. Pour mener à
  67 bien ce projet, plusieurs verrous tant théoriques que techniques devront
  68 être levées, nous les détaillons dans la suite de ce document.
  69
  70 \section{Point de départ}
  71 \label{sec:point-de-depart}
  72
  73 La conception d'un analyseur statique est complexe et elle est très
  74 consommatrice en temps. Nous comptons nous appuyer sur la plate forme
  75 collaborative issue du projet ANR ASOPT (auquel certains auteur de ce
  76 document ont participé) pour développer notre analyseur de modèles
  77 Matlab/Simulink. La plateforme ASOPT définit tous les
  78 éléments nécessaires à la conception et à l'utilisation d'un analyseur
  79 statique de programmes C. En particulier elle se fonde sur~:
  80 \begin{itemize}
  81 \item un traducteur de C vers un langage intermédiaire~: Newpseak
  82 \item une bibliothèque de domaines numériques abstraits~: Apron
  83 \item un solveur d'équations sémantiques~: Fixpoint
  84 \end{itemize}
  85 Ces éléménts (représentés en rouge dans la
  86 figure~\ref{fig:architecture-logicielle}) sont indispensable à la
  87 conception d'un analyseur statique~: le programme initial est traduit en
  88 Newspeak, puis le solveur Fixpoint tente de résoudre les équations
  89 sémantique générées par le programme. Pour cela, Fixpoint utilise un
  90 domaine abstrait choisi dans la bibliothèque APRON. Nous cherchons à
  91 reproduire cette démarche pour l'analyse de modèles Simulink.
  92
  93 \section{Objectifs et difficultés théoriques du projet}
  94 \label{sec:objectifs-difficultes}
  95
  96 Cette section doit servir à définir clairement le but du projet et les
  97 difficultés auxquelles nous nous attendons.
  98
  99 \subsection{Que veut dir ``analyser un modèle Simulink'' ?}
 100 \begin{itemize}
 101 \item Analyse d'un programme~: bien connu et chemin balisé car
 102   sémantique claire.
 103 \item Simulink = outil de prototypage rapide et de simulation
 104 \item pas de sémantique formelle autre que celle de la simulation,
 105   langage très riche (beaucoup de boîtes)
 106 \item Sémantique $\approx$ simulation, donc dépend de paramètres
 107 \item Modèles hétérogènes (temps discret/continu) $\Rightarrow$ même
 108   sémantique pour les deux parties ?
 109 \item Il faut donc se poser la question de la sémantique des modèles
 110   Simulink~: sémantique parfaite (i.e. solution de l'ODE) ou sémantique
 111   simulée (i.e. simulation de l'ODE), les deux ?
 112 \item La sémantique de Simulink devra probablement faire intervenir une
 113   notion de temps qui n'est pas triviale~: temps discret ou temps
 114   continu ? Cette notion de temps demandera probablement des domaines
 115   abstraits spécifiques sensiblement différents des domaines numérique existant.
 116 \item On pourra s'appuyer sur les travaux d'A. Chapoutot pour cette partie.
 117 \end{itemize}
 118
 119
 120 \subsection{Quel type d'analyse veut-on mener ?}
 121 Une fois une sémantique formelle bien définie, il faut se poser la
 122 question des propriétés importantes que l'on veut pouvoir prouver sur
 123 ces systèmes. Là encore, la présence du temps (continu ou discret) dans
 124 la sémantique de Simulink laisse à penser que les propriétés les plus
 125 intéressantes ne seront pas uniquement des invariants sur les variables
 126 du modèle mais peut-être des bornes sur l'évolution temporelle de ces
 127 variables. Plusieurs analyses de systèmes temporisés ont déjà été
 128 menées, il faut voir desquelles on souhaite s'inspirer~:
 129 \begin{itemize}
 130 \item analyse de J. Bertrane.
 131 \item analyse d'atteignabilité en système hybride.
 132 \item preuve de formule LTL sur les automates temporisés.
 133 \end{itemize}
 134
 135
 136 \subsection{Quel type de modèle veut-on analyser ?}
 137 Comme dit dans la Section~\ref{sec:contexte}, le langage Simulink est
 138 très large avec de nombreuses bibliothèques spécialisées dans certains
 139 métiers. Nous devrons donc identifier un sous-ensemble de blocs Simulink
 140 suffisemment riche pour permettre d'exprimer des lois de
 141 contrôle-commande non triviales mais dont nous sommes capables
 142 d'exprimer une sémantique formelle. Ce sous-ensemble comprendra au
 143 moins~:
 144 \begin{itemize}
 145 \item les blocs arithmétiques,
 146 \item les blocs intégrateur et retardateur,
 147 \item le saturateur,
 148 \item le bloc de zero-crossing detection.
 149 \end{itemize}
 150
 151
 152 \section{Vers l'analyse de Simulink~: une esquisse de plan de travail}
 153 \label{sec:vers-l-analyse-de-simulink}
 154
 155 L'architecture logicielle d'un analyseur de Matlab/Simulink est donnée
 156 à la figure~\ref{fig:architecture-logicielle}. Elle s'appuie très
 157 largement sur la plate-forme Newpseak-Apron-Fixpoint. Les éléments en
 158 rouge sont les éléments existant et les éléments en bleu sont les
 159 éléments à ajouter.
 160
 161 Une suite au projet ANR ASOPT pourrait permettre la mise en {\oe}uvre
 162 d'un analyseur statique de Matlab/Simulink. Les premières éléments de
 163 réflexion sont donnés dans la suite.
 164
 165 \begin{figure}[t]
 166   \centering
 167   \begin{tikzpicture}[node distance=1.4cm]
 168     \tikzstyle{every node}=[draw, ultra thick];
 169
 170     \node[ellipse, fill=green!20] (mdl) {mdl files};
 171
 172     \node[ellipse, fill=green!20] (c_ada) [left of=mdl, node
 173     distance=6cm] {C/Ada files};
 174
 175     \node[rectangle, dashed, fill=blue!20] (parser) [below of=mdl] {parser:
 176       Simulink to Newspeak};
 177
 178     \node[rectangle, fill=red!20] (parser2) [below of=c_ada]
 179     {parser: C/Ada to Newspeak};
 180
 181     \node[ellipse, dashed, fill=blue!20] (newspeakode) [below of=parser]
 182     {Newpseak with annoted ODEs};
 183
 184     \node[rectangle, dashed, fill=blue!20] (pass2) [below of=newspeakode]
 185     {discretized state part};
 186
 187     \node[rectangle, dashed, fill=blue!20, node distance=4cm] (pass1) [left
 188     of=pass2] {output part};
 189
 190     \node[rectangle, dashed, fill=blue!20, node distance=5cm] (pass3)
 191     [right of=pass2] {guaranteed state part};
 192
 193     \node[ellipse, fill=red!20] (newspeak) [below of=pass2]
 194     {Newspeak};
 195
 196     \node[rectangle, fill=red!20] (npk2syntax) [below of=newspeak]
 197     {parser: npk2syntax};
 198
 199     \node[ellipse, fill=red!20] (syntax) [below of=npk2syntax]
 200     {syntax};
 201
 202     \node[rectangle, dashed, fill=blue!20] (hyfixpoint) [below
 203     of=syntax] {Hybrid Fixpoint};
 204
 205     \node[rectangle, dashed, fill=blue!20] (hyapron) [left
 206     of=hyfixpoint, node distance=4cm] {Sequence domain};
 207
 208     \node[rectangle, thick, fill=red!20] (fixpoint) [below
 209     of=hyfixpoint] {Fixpoint};
 210
 211     \node[rectangle, thick, fill=red!20] [left of=fixpoint,
 212     node distance=4cm] (apron) {Apron};
 213
 214     \node[rectangle, dashed, fill=blue!20] [right of=fixpoint,
 215     node distance=4cm] (acceleration) {Acceleration};
 216
 217     \node[rectangle, thick, fill=red!20] [below of=fixpoint,
 218     node distance=1.5cm] (ptr) {Ptr};
 219
 220     \draw[->] (mdl) -- (parser);
 221
 222     \draw[->] (parser) -- (newspeakode);
 223
 224     \draw[->] (newspeakode) -- (pass1);
 225
 226     \draw[->] (newspeakode) -- (pass2);
 227
 228     \draw[->] (newspeakode) -- (pass3);
 229
 230     \draw[->] (pass1) -- (newspeak);
 231
 232     \draw[->] (pass2) -- (newspeak);
 233
 234     \draw[<->, dashed] (pass3) |- node[draw=none,right, near start] {GRKLib?}
 235     (hyfixpoint.east);
 236
 237     \draw[->] (newspeak) -- (npk2syntax);
 238
 239     \draw[->] (npk2syntax) -- (syntax);
 240
 241     \draw[->] (syntax) -- (hyfixpoint);
 242
 243     \draw[<->] (hyfixpoint) -- (fixpoint);
 244
 245     \draw[<->] (hyapron) -- (apron);
 246
 247     \draw[<->] (hyapron) -- (hyfixpoint);
 248
 249     \draw[<->] (fixpoint) -- (apron);
 250
 251     \draw[<->] (fixpoint) -- (ptr);
 252
 253     \draw[<->] (fixpoint) -- (acceleration);
 254
 255     \draw[<->] (hyfixpoint.base east) -| (acceleration);
 256
 257     \draw[->] (c_ada) -- (parser2);
 258
 259     \draw[->] (parser2) |- (newspeak);
 260   \end{tikzpicture}
 261   \caption{Architecture logicielle d'un analyseur de Matlab/Simulink}
 262   \label{fig:architecture-logicielle}
 263 \end{figure}
 264
 265 \subsection{Traduction Simulink vers Newspeak}
 266 \label{sec:traduction-simulink-vers-newspeak}
 267
 268 Les modèles Matlab/Simulink mélangent des équations différentielles et
 269 des équations récurrentes pour modéliser respectivement des systèmes à
 270 temps continu et des systèmes à temps discret.
 271
 272 \textbf{Problématique}~: Newspeak a été conçu pour modéliser des
 273 programmes impératifs écrits en C ou en Ada. Comment adapté le langage
 274 Newspeak pour décrire des équations différentielles? Ou plus
 275 généralement comment adapter Newspeak pour représenter l'environnement
 276 physique d'un programme?
 277
 278 \subsection{Nouveaux domaines Apron}
 279 \label{sec:nouveaux-domaines-apron}
 280
 281 Les modèles Matlab/Simulink décrivent l'évolution d'un système
 282 logiciel et environnement phy\-sique au cours du temps. L'objectif
 283 d'une analyse statique de ces modèles est alors d'inférer de nouveaux
 284 types d'invariants permettant de caractériser cette évolution
 285 temporelle. Ces invariants pourrait être ainsi utilisés pour la
 286 vérification fonctionnelle des systèmes.
 287
 288 \textbf{Problématique}~: Apron est une bibliothèque de domaines
 289 numériques abstraits qui ne sont pas destinés à la modélisation de
 290 propriétés temporelles. Ajouter un nouveau domaine (ou une sur-couche
 291 aux domaines) pour ce nouvel objectif tout en gardant les interfaces
 292 existantes de Apron.
 293
 294 \subsection{Nouvel itérateur de point fixe}
 295 \label{sec:nouvel-iterateur-de-point-fixe}
 296
 297 Pour manipuler un domaine permettant d'inférer des propriétés
 298 temporelles, il semble nécessaire de modifier également la façon de
 299 résoudre les équations sémantiques.
 300
 301 \textbf{Problématique}~: Modifier Fixpoint (ou ajouter une sur-couche
 302 à Fixpoint) pour inférer des propriétés temporelles.
 303
 304 \subsection{Méthodes d'accélération de la convergence}
 305 \label{sec:methodes-d-acceleration-de-la-convergence}
 306
 307 La résolution du calcul de point fixe peut être coûteuse en temps donc
 308 il faut mettre en place des méthodes pour accélérer ce calcul.
 309
 310 \textbf{Problématique}~: Ajouter les méthodes d'accélération par les
 311 méthodes numériques dans le solveur Fixpoint et la bibliothèque Apron.
 312
 313 \end{document}