9-Annexes.tex

%%
%%  Annexes.
%%
%%  Note: Ne pas modifier la ligne ci-dessous.
\addcontentsline{toc}{compteur}{ANNEXES}
%%
%%
%%  Toutes les annexes doivent être inclues dans ce document
%%  les unes à la suite des autres.

\begin{landscape}
\Annexe{Types de propriétés supportés par différents model-checkers}
\begin{table}[ht]
\centering
\caption{Types de propriétés prises en charge par les outils présentés.}
\begin{tabular}{|l|c|c|c|c|c|c|c|c|c|}
\hline
Outils     & \multicolumn{9}{c|}{Types de propriétés vérifiées}                                                                                     \\
           & Assertions   &      LTL     & Arithmétique &     Tableaux & Pointeurs    & Data races   & Deadlock     & Cast         & Init           \\ \hline
SPIN       &              & $\checkmark$ &              &              &              &              &              &              &                \\
Pancam     & $\checkmark$ &              &              &              &              &              &              &              &                \\
Inspect    & $\checkmark$ &              &              &              &              &              &              &              &                \\
Divine     & $\checkmark$ & $\checkmark$ &              &              &              &              &              &              &                \\
CIVL       & $\checkmark$ &              & $\checkmark$ & $\checkmark$ & $\checkmark$ & $\checkmark$ & $\checkmark$ & $\checkmark$ & $\checkmark$   \\
Impara     & $\checkmark$ &              &              &              &              &              &              &              &                \\
Satabs     & $\checkmark$ &              & $\checkmark$ & $\checkmark$ & $\checkmark$ &              &              &              &                \\
Threader   & $\checkmark$ &              &              &              &              &              &              &              &                \\
CPAChecker & $\checkmark$ &              &              &              &              &              &              &              &                \\
CBMC       & $\checkmark$ &              & $\checkmark$ & $\checkmark$ & $\checkmark$ &              &              &              &                \\
ESBMC      & $\checkmark$ &              & $\checkmark$ & $\checkmark$ & $\checkmark$ & $\checkmark$ & $\checkmark$ &              &                \\
CSeq       & $\checkmark$ &              &              &              &              &              &              &              &                \\
Lazy-CSeq  & $\checkmark$ &              &              &              &              &              & $\checkmark$ &              &                \\
Mu-CSeq    & $\checkmark$ &              &              &              &              &              &              &              &                \\
UL-CSeq    & $\checkmark$ &              &              &              &              &              &              &              &                \\ \hline
\end{tabular}
\label{tab:prop_type_table}
\end{table}

\end{landscape}



\Annexe{Exemple de spécification}

Dans cette annexe, nous présentons un exemple détaillé de spécification et de
vérification d'un problème simple à l'aide de baProduct. Nous détaillons les
étapes intermédiaires.

Considérons le problème suivant : un système contient deux batteries. Les
batteries se vident simultanément au fil de l'utilisation. Lorsqu'une batterie
est épuisée, elle est remplacée. Une batterie est suffisante pour que le système
fonctionne, cependant, si les deux batteries sont vides en même temps, le
système n'a plus d'énergie et cesse de fonctionner.

Un tel système peut être modélisé par le code ci-dessous. Deux threads,
\texttt{battery1} et \texttt{battery2} contrôlent le rythme auquel les
batteries se vident. Le pourcentage d'énergie dans la batterie est représenté
par la variable \texttt{energy}. Celle-ci est décrémentée dans une
boucle, ce qui représente la consommation de l'énergie, avant d'être remise à
une valeur de 10, ce qui simule le remplacement. Dans ce système simpliste,
aucune synchronisation n'existe entre les threads.
On peut aussi noter que la boucle principale des threads ne s'exécute que trois
fois, afin que la trace soit finie. Dans un cas d'utilisation réel, on
utiliserait une boucle infinie et les options du model-checker permettraient de
limiter le nombre de dépliages, mais pour des raisons de simplicité, nous codons
directement ce comportement.

\noindent\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Thread 1]
void* battery1(void* d) {
  int energy;
  int i;
  // Initialization
  energy = 10;
  for(i=0; i<3; i++) {
    // Empty the battery
    while (energy > 0)
        energy--;
    // Replace the battery
    energy = 10;
  }
  pthread_exit(NULL);
}
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Thread 2]
void* battery2(void* d) {
  int energy;
  int i;
  // Initialization
  energy = 10;
  for(i=0; i<3; i++) {
    // Empty the battery
    while (energy > 0)
        energy--;
    // Replace the battery
    energy = 10;
  }
  pthread_exit(NULL);
}
\end{lstlisting}
\end{minipage}

Pour s'assurer que le système fonctionne correctement, on souhaite s'assurer
qu’une des deux batteries a toujours un niveau d'énergie supérieur à 20\%, une
fois le système initialisé.

Nous allons tout d'abord spécifier cette propriété sur le système. Pour cela, on
délimite tout d'abord les zones de validités. L'initialisation des batteries ne
doit pas en faire partie, mais la boucle principale du programme y est incluse.

\noindent\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Thread 1 avec labels]
void* battery1(void* d) {
  int energy;
  int i;
  energy = 10;
b1: for(i=0; i<3; i++) {
    // Empty the battery
    while (energy > 0)
        energy--;
    // Replace the battery
    energy = 10;
  }
e1: pthread_exit(NULL);
}
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Thread 2 avec labels]
void* battery2(void* d) {
  int energy;
  int i;
  energy = 10;
b2: for(i=0; i<3; i++) {
    // Empty the battery
    while (energy > 0)
        energy--;
    // Replace the battery
    energy = 10;
  }
e2: pthread_exit(NULL);
}
\end{lstlisting}
\end{minipage}

On définit ensuite les fonctions d'évaluation. Ici, nous allons utiliser deux
propositions atomiques, chacune indiquant si une batterie a un niveau
d'énergie faible. Cependant, une seule fonction d'évaluation est nécessaire
puisque les deux propositions atomiques s'évaluent selon la même formule.

\begin{lstlisting}[language=C, frame=single, caption=Fonction d'évaluation]
int low_power(int energy) {
  return energy <= 2;
}
\end{lstlisting}

Il ne reste alors qu'à exprimer la spécification en elle même.

\pagebreak

\begin{lstlisting}[frame=single, caption=Spécification]
{ "ltl": "G(! (p1 && p2))",
  "pa": [
    {"name": "p1",
      "default": false,
      "expr": "low_power",
      "span": ["b1", "e1"],
      "params": ["battery1::energy"]
    },
    { "name": "p2",
      "default": false,
      "expr": "low_power",
      "span": ["b2", "e2"],
      "params": ["battery2::energy"]
    }
  ]
}
\end{lstlisting}

On utilise alors baProduct pour instrumenter ce code. On utilise pour cela
la commande \texttt{baProduct.py -i battery.c -s battery.spec}. Cette commande
réalise tout d'abord un appel à LTL2BA afin de générer l'automate correspondant
à la négation de la formule LTL (étape 1 dans la
Figure~\ref{fig:baProduct_func}). On obtient l'automate en
Figure~\ref{fig:ba_battery}.

\begin{figure}[ht]
\begin{center}
  \includegraphics[height=0.2\textheight]{ba_battery.png}
\end{center}
\caption{Automate de Büchi généré par LTL2BA pour la spécification des
batteries.}
\label{fig:ba_battery}
\end{figure}

Cet automate est ensuite représenté en C. On obtient le code suivant (on suppose
ici que CBMC va être utilisé comme backend).

\begin{lstlisting}[language=C, frame=single, caption=Automate encodé en C]
// Current values of atomic propositions
int _ltl2ba_atomic_p1 = 0;
int _ltl2ba_atomic_p2 = 0;
// Is a proposition atomic in its validity area ?
int _ltl2ba_active_p1 = 0;
int _ltl2ba_active_p2 = 0;
// In a validity area, point to local variables
// used in evaluation functions
int *_ltl2ba_pointer_thread2_energy = 0;
int *_ltl2ba_pointer_thread1_energy = 0;
// Current state of the automaton
int _ltl2ba_state_var = 0;

// Transition function of the automaton
void _ltl2ba_transition() {
  int choice = nondet_uint(); // Choose a transition
  switch (_ltl2ba_state_var) {
  case 0: // Transitions from state 0
    if (choice == 0) {
      __CPROVER_assume(_ltl2ba_atomic_p1 && _ltl2ba_atomic_p2);
      _ltl2ba_state_var = 1;
    } else if (choice == 1) {
       __CPROVER_assume(1);
       _ltl2ba_state_var = 0;
    } else {
       __CPROVER_assume(0);
    }
    break;
  case 1: // State one is an accepting pit
    __CPROVER_assert(0, "ERROR_SURE");
    break;
  }
}

// Pre-calculated results for stutter acceptance
int _ltl2ba_surely_reject[2] = {0, 0};
int _ltl2ba_surely_accept[2] = {0, 1};
int _ltl2ba_stutter_accept[8] = {0, 1, 0, 1, 0, 1, 1, 1,};

int _ltl2ba_sym_to_id() {
  int id = 0;
  id |= (_ltl2ba_atomic_p2 << 1);
  id |= (_ltl2ba_atomic_p1 << 0);
  return id;
}
// Raise an assertion according to the final state
void _ltl2ba_result() {
  // The automaton accept the word, whatever the suffix
  int reject_sure = _ltl2ba_surely_accept[_ltl2ba_state_var];
  __CPROVER_assert(!reject_sure, "ERROR SURE");
  // The automaton accept the word in stutter-extension semantic
  int id = _ltl2ba_sym_to_id();
  int accept_stutter =_ltl2ba_stutter_accept[id * 2
                                             + _ltl2ba_state_var];
  __CPROVER_assert(!accept_stutter, "ERROR MAYBE");
  // The automaton does not surely reject the word
  int valid_sure = _ltl2ba_surely_reject[_ltl2ba_state_var];
  __CPROVER_assert(valid_sure, "VALID MAYBE");
}
\end{lstlisting}

Le code est ensuite instrumenté pour construire le produit avec l'automate
(étape 2 dans la Figure~\ref{fig:baProduct_func}).

\begin{lstlisting}[language=C, frame=single, caption=Code instrumenté]
void *battery1(void *d )
{
  int energy ;
  int i;
  energy = 10;
  // Beginning of the validity area
  // Open an atomic bloc
  __CPROVER_atomic_begin();
  _ltl2ba_pointer_thread1_energy = &energy;
  _ltl2ba_atomic_p1 =
      low_power(*_ltl2ba_pointer_thread1_energy);
  _ltl2ba_active_p1 = 1;
  _ltl2ba_transition();
  __CPROVER_atomic_end();
  b1: for(i=0; i<3; i++) {
    while (energy > 0) {
      // Variable modification
      __CPROVER_atomic_begin();
      energy--;
      // Compute the new value of the atomic proposition
      _ltl2ba_atomic_p1 =
          low_power(*_ltl2ba_pointer_thread1_energy);
      // Take a transition in the automaton
      _ltl2ba_transition();
      __CPROVER_atomic_end();
    }
    __CPROVER_atomic_begin();
    energy = 10;
    _ltl2ba_atomic_p1 =
        low_power(*_ltl2ba_pointer_thread1_energy);
    _ltl2ba_transition();
    __CPROVER_atomic_end();
  }
  // End of the validity area
  __CPROVER_atomic_begin();
  // Set the atomic proposition to the default value
  _ltl2ba_atomic_p1 = 0;
  // Deactivate the atomic proposition
  _ltl2ba_active_p1 = 0;
  // Take a transition in the automaton
  _ltl2ba_transition();
  __CPROVER_atomic_end();
e1: pthread_exit(0);
}
void *battery2(void *d )
{
  int energy ;
  int i;
  energy = 10;
  __CPROVER_atomic_begin();
  _ltl2ba_pointer_thread2_energy = & energy;
  _ltl2ba_atomic_p2 = low_power(*_ltl2ba_pointer_thread2_energy);
  _ltl2ba_active_p2 = 1;
  _ltl2ba_transition();
  __CPROVER_atomic_end();
  b2: for(i=0; i<3; i++) {
    while (energy > 0) {
      __CPROVER_atomic_begin();
      energy--;
      _ltl2ba_atomic_p2 =
          low_power(*_ltl2ba_pointer_thread2_energy);
      _ltl2ba_transition();
      __CPROVER_atomic_end();
    }
    __CPROVER_atomic_begin();
    energy = 10;
    _ltl2ba_atomic_p2 =
        low_power(*_ltl2ba_pointer_thread2_energy);
    _ltl2ba_transition();
    __CPROVER_atomic_end();
  }
  __CPROVER_atomic_begin();
  _ltl2ba_atomic_p2 = 0;
  _ltl2ba_active_p2 = 0;
  _ltl2ba_transition();
  __CPROVER_atomic_end();
e2: pthread_exit(0);
}
int main(int argc , char **argv )
{
  pthread_t t1 ;
  pthread_t t2 ;
  pthread_create(&t1, 0, &battery1, 0);
  pthread_create(&t2, 0, &battery2, 0);
  pthread_join(t1, 0);
  pthread_join(t2, 0);
  __CPROVER_atomic_begin();
  _ltl2ba_result();
  __CPROVER_atomic_end();
  return 0;
}
\end{lstlisting}

Il ne reste plus qu'à vérifier ce code instrumenté à l'aide d'un model-checker.
Ici, nous avons utilisé CBMC, à l'aide de la commande \texttt{cbmc
  battery\_instr.c}. La sortie indique que l'assertion \texttt{ERROR\_SURE} a été
violée : une erreur est donc détectée de manière certaine dans le code.