---
title: "Conception formelle : introduction"
date: 2023-01-06
tags: ["Bugs", model-checking"]
categories: ["Conception formelle", "Cours"]
mathjax: true
---

## Pourquoi?

### Un peu d'histoire: les bugs célèbre

### 1985 : Banque de New-York

Un entier passe de 32768 à 0, conséquence : 2 jours d'interruption de service et
24 milliards de dollars d'emprunt et plus de 5 millions de perte.

### 1990: AT&T

Un `break` est oublié dans un `case` comme dans l'exemple ci-dessous:

```c
switch(i) {
    case 1 : function1(); break;
    case 2 : function2(); // a forgotten break;
    default: defaultfunction();
}
```

75 millions d'appels téléphonique dans le vide, pour *American Airline*, 200 000
réservations en moins. Heureusement AT&T utilisait déjà le réseau pour les
déploiement. Si la propagation du bug a été accélérée, le **déploiement du
patch** aussi.

### 1994 : bug du Pentium

Une erreur de calcul dans une fonction très particulière de processeur
entrainait une erreur de calcul. La réponse d'*Intel* fut peu sympathique à
l'époque qui assurait que peu de personnes utilisaient cette fonction etdonc
**qu'ils ne fixeraient pas** le problème.

Depuis, *Intel* publie les preuves de calculs de leurs processeurs, tout
comme *AMD*.

### 1996 : Ariane 5

Destruction de la fusée après 39 secondes de vol suite à deux grandes erreurs :

 1. conversion d'un entier 64 bits vers 16 bits avec overflow
 2. les deux ordinateurs utilisés pour la redondance partageaient le même code. 
    Le bug était donc présent sur les deux machines.

### 1985 - 1987 : Thernac 25

Nous sommes ici en présence du premier bug ayant tué un humain. Le Thernac
25][l_thernac] était une machine utilisée en radiothérapie pour le traitement
des cancers. Des patient se sont plaint de sensation de forte brulure lors de
séances. Il a fallut attendre trois ans et au moins **4 morts** pour que le
fabricant rappelle ce modèle et mène l'investigation

[l_thernac 25]: https://fr.wikipedia.org/wiki/Therac-25

## Besoin de fiabilité

Dès les années 1990, il y a une prise de conscience générale de la **nécessité**
de garanties pour le développement logiciel. Ce qui comprend ben entendu **les
test** effectués sur le code, l'**uniformisation** de la sémantique utilisée(UML
-- *Universal Modelisation Laguage*), les **design patterns**.

## Panorama des méthodes formelles

Le but des méthodes formelles est de raisonner autour des logiciels pour
déterminer les contrôles et comportements par les **méthodes mathématiques**.

Il faut pour cela obtenir un modèle former par l'analyse et le tester.

 * est-ce que le modèle est le bon, est-il correct? : **la validation**
 * pouvons nous vérifier le modèle? : **la décidabilité**[^n_decidabilite]
 * pouvons nous traduire les résultats? : **l'abstraction**

[^n_decidabilite] ne proposition (on dit aussi énoncé) est dite décidable dans
une théorie axiomatique si on peut la démontrer ou démontrer sa négation dans le
cadre de cette théorie. Un énoncé mathématique est donc indécidable dans une
théorie s'il est impossible de le déduire, ou de déduire sa négation, à partir
des axiomes de cette théorie. Source [Wikipedia](https://fr.wikipedia.org/wiki/D%C3%A9cidabilit%C3%A9)

### Pour qui?

Les méthodes coûtent cher et le personnel qualifié manque. Par conséquent seul
les entreprises développant des systèmes complexes et/ou critiques les
utilisent.

Quelques précisions :

 * **complexes** : beaucoup d'interactions entre les composants
 * **critiques** : important, que se soit économiquement, humainement ou les
   deux.

### Les outils

L'idée derrière ce type d'outils: **manipuler les preuves** : un programme est
un théorème, est-il adapté? C'est**un autre problème**.

Ces outils ne sont pas entièrement automatiques.

#### Interprération abstraite

Transformer une problème concret en un problème abstrait plus simple, rendant la
preuve plus facile à produite

\\( \(M_{\text{concret}} \models \phi\) \implies \( M_{\text{abstrait}} \models \phi \) \\)

#### Vérification du modèle

Prendre en entrée un modèle \\(M\\), une spécification \\(\phi\\). ON vérifie
alors que \\(M\ \models \phi \).

#### Raffinement et implémentation

Autoriser la transformation d'une spécification en implémentation tout en
préservant à chaque étapes les propriétés essentielles à notre système.

#### Gestion des tests

Génération de séquences de tests sur le modèle d'après la spécification. Ces
tests dépendent du but recherchés.

Les test de **conformités** sont utilisés pour valider le vrai système. Les
tests **d'interopérabilité** valident le système dans un contexte ouvert.

#### Système Stochastique

Utiliser les chaines de [Markov][l_markov] et les [processus stochastique]
[l_stockas] pour étudier la probabilité qu'un évènements se produise.

## Choix de la méthode

![Schéma en V, source Alain Griffault](./imgs/schema_v.png)

Il n'y a pas une méthode à choisir, plusieurs méthodes formelles à appliquer en
fonction de la position dans le cycle.

### model checking

N'utilisons pas les données mais prouvons les interaction inter-modules :

  * pour clarifier le *cahier des charges*
  * pour aboutir un *cahier des charges*

### Preuve de théorème

Ici nous validons l'algorithme afin de prouver qu'il fonctionne. Nous pouvons
alors implémenter soir dans un langage généraliste, soir dans un langage dédié
(donc spécifique). On obtient alors **un code certifié**.

### Analyse de code binaire

Obtenir des garanties sur le code binaire --  qu'ils ne perturbent pas le
système -- sans pour autant avoir le code source.

```
code source -> décompilation -> modèle -> analyse
```

### Génération de tests

Génération de tests pertinents pour notre application partir du modèle et du
cahier des charges.

[l_markov]:https://fr.wikipedia.org/wiki/Processus_de_Markov
[l_stockas]:https://fr.wikipedia.org/wiki/Processus_stochastique