Add second part of verification

content/conception_formelle/2_verification/index.md

@@ -224,7 +224,82 @@ transitions:
    \\(T\\) comme transitions
  * \\(\text{coreach}(S,T)\\) représente tous les états avec comme destnation
    \\(S\\) et utilisants \\(T\\) comme transitions.
- * \\(\text{loop}(T_1,T_2)\\) représente les *Strongly Connected Components*
-   (SCC). C'est une formule de transition tel que \\(T_3 \subseteq T_2\\) et
-   \\(T_3 \cap T_1 \neq \emptyset\\)
- 
+ * \\(\text{loop}(T_1,T_2)\\) calcule des transition, elle représente les
+   *Strongly Connected Components* (SCC). C'est une formule de transition tel
+   que \\(T_3 \subseteq T_2\\) et \\(T_3 \cap T_1 \neq \emptyset\\). Ces *SCC*
+   déterminent toutes situations permettant de revenir à la situation initiale.
+
+## ARC
+
+*ARC* est le *model checker* d'Altarica, c'est un interpréteur de commande.
+
+### Les propriétés
+
+En plus des propriétés heritées de la logique de *Dicky*, il existe dans ARC les
+propriété calculées suivantes pour chaque nœud:
+
+ * `epsilon` :
+ * `self` : transitions dont la source est la destination sont égaux
+ * `self-epsilon`L définis par \\(epsilon \cap self \\)
+ * `not_deterministic`: ensemble de transition non déterministe definies plus
+   formellement par
+   \\(\\{(s,e,t_1) \in E | \exists t_2 /in V, (s,e,t_2) \in  E\\}\\)
+
+#### Exemple
+
+```
+with Switch, CircuitV1, Scheduler do
+    deadlock := any_s - src(any_t - self_epsilon);
+    notSCC := any_t - loop(any_t, any_t);
+done
+with CircuitV1, CircuitV2, CircuitV1_OK do
+    bug := [L.on & ~L.ok];
+    notControl := (label G.failure | label L.reaction | epsilon) - self_epsilon;
+    
+    // IR means infinite reactions
+    IR := loop(notControl, notControl);
+done
+```
+### Les opérateurs
+
+En plus des oérateurs disponibles dnas la logique de Dicky, ARC implémente les
+opérateurs suivants:
+
+ * \\(trace(S_1, T, S_2)\\) : ensemble de transitions représentant le chemin le
+   plus long de \\(S_1\\) vers \\(S_2\\) en utilisant les transitions\\(T\\).
+ * \\(project(S,T, 'newNodeName', boolean, aNode)\\) : construit une nouveau
+   nœud AltaRica avec toutes les transitions \\(T\\) prenant leurs origines dans
+   \\(S\\) en restectant les déclarations de \\(aNode\\) (cette déclaration est
+   facultative).
+
+`trace` nous sera utile pour trouver des contre-exemple et `project` pour
+calculer des contrôleurs pour notre système.
+
+### Methodologie
+
+nous allons utiliser cet outils ocmme un **déboggeur de modèle**, en respectant
+les étapes suivantes:
+
+ 1. identifier les composants de base
+ 2. choisir entre le design *fonctionnel* ou *architectural* en fonction de
+    l'objectif et de ce que l'on sait faire.
+ 3. choisir entreun système **ouvert** ou **fermé** (restreindre le système a
+    des cas d'utilisation)
+ 4. construire l'arborescence du bas vers le haut
+
+### Validation d'un premier modèle
+
+ 1. validation de la topologie du graphe (*SCC*, *deadlock*)
+ 2. propriété dépendantes de l'application (pas de réaction infinie)
+ 3. toues les évèmements sont utiles
+ 4. visualisation de petits composants
+ 5. simutation
+
+les étapes 1 et deux sont à répéter jusqu'à obtention d'un modèle valide.
+
+### Vérification du modèle
+
+Les spécification son écrites comme une liste de propiété logique et utilise la
+logique de *Dicky* enrichie des éléments vu dans cette partie. Pour chacune des
+propriétés ne satifaisant pas le modèle, **un contre exemple le plus petit
+possible doit être calculé**.