171 lines
5.9 KiB
Markdown
171 lines
5.9 KiB
Markdown
---
|
|
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
|
|
|
|
|
|
|
|
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
|