www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs

cours-2011-11-04.tex (3226B)

      1 \documentclass[a4paper,french]{article}
      2 \usepackage[T1]{fontenc}
      3 \usepackage[utf-8]{inputenc}
      4 \usepackage[frenchb]{babel}
      5 \begin{document}
      6 Documentation LOTOS (Language Of Temporal\footnote{Temporel et non temporisé : ordonnancement et non temps d'exécution} Ordering Specification) :
      7 \texttt{/usr/local/cadp/doc/pdf/Garavel-89-*} (structures de contrôle).
      8 Langage LOTOS normalisé ISO en 1989.
      9 
     10 Algèbre = ensemble de termes construits par des opérations algébriques.
     11 \begin{itemize}
     12 \item Basic LOTOS = algèbres de processus\marginpar{comportement} (CCS + CSP).
     13 \begin{itemize}
     14 \item Termes = processus (+ actions)?
     15 \item Opérateurs = prefix ($;$), choice ($[]$), parallel ($||\ |[]|\  |||$), enable ($>>$)\footnote{«Composition séquentielle de processus». $P >> Q$ exécute $P$ jusqu'à ce que $P$ se termine en déclenchant l'action delta (exit), après quoi on exécute $Q$)}, disable ($[>$)
     16 \end{itemize}
     17 \item ACT One = ADT (Abstract Data Type).
     18 \end{itemize}
     19 
     20 % $[>$ : PxP->P
     21 %        P ->^a P' (Q -/->^a)
     22 % [> (1) --------------------
     23 %        P[>Q ->^a P' [> Q
     24 %
     25 %             Q ->^a Q'
     26 %    (2) --------------------
     27 %           P[>Q ->^a Q'
     28 
     29 L'environnment avec lequel le LTS interagit n'a pas connaissance de l'état du LTS.
     30 
     31 Le LTS décrit les séquencs d'actions \emph{possibles}.
     32 
     33 % SECTION 5
     34 \section{Comparaisons entre processus}
     35 
     36 % . ->^a . ->^b .^0 =^? . ->^a . ->^i . ->^b .^0
     37 
     38 Objectif: Véifier les modlèles.
     39 Def: Vérifier = $Spécification(ou modèle de conception) |=(satisfait) Propriétés$
     40 S : Spec en LTS
     41 P : propdans un autre langage (calcul propositionnel, Logique Temporelle Linéaire, Computational Tree Logic, \dots)
     42 
     43 Exemple : vérifier que $a$ est toujours suivi de $b$. Que signifie "toujours suivi" ?
     44 Interprétation possible : (P[a,b,c,d,\dots] |[a,b]| E[a,b]) avec E[a,b]:=a;b;E[a,b] s'exécute sans blocage. Cela signifie que après avoir fait $a$, on pourra \emph{un jour} exécuter $b$.
     45 
     46 On distingue la vérification de la validation. Vérif = comparaison entre deux choses exprimées formellment. Validation = s'assurer que le système est bien celui souhaité. «Le système est-il construit correctement ?» vs. «Le système est-il le bon ?»
     47 
     48 Nous utiliserons un LTS pour la spec, et un LTS pour la réalisation (moins abstrait).
     49 
     50 \subsection{Équivalence forte}% 5.1
     51 Définition : P et Q sont forement équivalents, ce que l'on note $P~Q$, ssi $\forall \alpha \in G\union{i}$, quel que soit $P ->^\alpha P'$,
     52 il existe $Q'$ tel que $Q ->^\alpha Q'$ et $P' ~ Q'$, et vice versa (quand Q fait une action, P sait la faire aussi).
     53 
     54 cf. Milner 89 Communication and Concurrency, HOARE, C.A.R., Prentice Hall
     55     Milner 99 Communicating and Mobile Systems: the Pi-Calculus, Cambridge University Press
     56 
     57 P:=a;i;b;stop ~/ (pas fortement eqv) Q:=a;b;stop
     58 
     59 %   /-a---b
     60 % P-           ~    P---a---b
     61 %   \-a---b
     62 Q peut "imiter" P.
     63 
     64 0 = stop
     65 P[]0 ~ P
     66 P|||0 ~ P
     67 P||0 ~ P
     68 P[]Q ~ Q[]P
     69 P|Q ~ Q|P valable pour ||, |||, |[]|
     70 P[](Q[]R) ~ (P[]Q)[]R
     71 P[]P ~ P
     72 
     73 0 élément neutre pour [] (addition) et || (mult.)
     74 <P,[],;> a une structure de monoïde.
     75 
     76 a;(P[]Q) ~/ (a;P) [] (a;Q)
     77 %Si on prend P:=b;0 et Q:=0, on a ". ->^a 0 ->^b -> 0" à gauche et . (/->^a 0) \->^a . ->^b 0
     78 
     79 \end{document}