Add introduction lecture

content/conception_formelle/1_introduction/index.md

@@ -0,0 +1,171 @@
+---
+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