79 lines
3.2 KiB
TeX
Executable File
79 lines
3.2 KiB
TeX
Executable File
\documentclass[a4paper,french]{article}
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage[utf-8]{inputenc}
|
|
\usepackage[frenchb]{babel}
|
|
\begin{document}
|
|
Documentation LOTOS (Language Of Temporal\footnote{Temporel et non temporisé : ordonnancement et non temps d'exécution} Ordering Specification) :
|
|
\texttt{/usr/local/cadp/doc/pdf/Garavel-89-*} (structures de contrôle).
|
|
Langage LOTOS normalisé ISO en 1989.
|
|
|
|
Algèbre = ensemble de termes construits par des opérations algébriques.
|
|
\begin{itemize}
|
|
\item Basic LOTOS = algèbres de processus\marginpar{comportement} (CCS + CSP).
|
|
\begin{itemize}
|
|
\item Termes = processus (+ actions)?
|
|
\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 ($[>$)
|
|
\end{itemize}
|
|
\item ACT One = ADT (Abstract Data Type).
|
|
\end{itemize}
|
|
|
|
% $[>$ : PxP->P
|
|
% P ->^a P' (Q -/->^a)
|
|
% [> (1) --------------------
|
|
% P[>Q ->^a P' [> Q
|
|
%
|
|
% Q ->^a Q'
|
|
% (2) --------------------
|
|
% P[>Q ->^a Q'
|
|
|
|
L'environnment avec lequel le LTS interagit n'a pas connaissance de l'état du LTS.
|
|
|
|
Le LTS décrit les séquencs d'actions \emph{possibles}.
|
|
|
|
% SECTION 5
|
|
\section{Comparaisons entre processus}
|
|
|
|
% . ->^a . ->^b .^0 =^? . ->^a . ->^i . ->^b .^0
|
|
|
|
Objectif: Véifier les modlèles.
|
|
Def: Vérifier = $Spécification(ou modèle de conception) |=(satisfait) Propriétés$
|
|
S : Spec en LTS
|
|
P : propdans un autre langage (calcul propositionnel, Logique Temporelle Linéaire, Computational Tree Logic, \dots)
|
|
|
|
Exemple : vérifier que $a$ est toujours suivi de $b$. Que signifie "toujours suivi" ?
|
|
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$.
|
|
|
|
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 ?»
|
|
|
|
Nous utiliserons un LTS pour la spec, et un LTS pour la réalisation (moins abstrait).
|
|
|
|
\subsection{Équivalence forte}% 5.1
|
|
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'$,
|
|
il existe $Q'$ tel que $Q ->^\alpha Q'$ et $P' ~ Q'$, et vice versa (quand Q fait une action, P sait la faire aussi).
|
|
|
|
cf. Milner 89 Communication and Concurrency, HOARE, C.A.R., Prentice Hall
|
|
Milner 99 Communicating and Mobile Systems: the Pi-Calculus, Cambridge University Press
|
|
|
|
P:=a;i;b;stop ~/ (pas fortement eqv) Q:=a;b;stop
|
|
|
|
% /-a---b
|
|
% P- ~ P---a---b
|
|
% \-a---b
|
|
Q peut "imiter" P.
|
|
|
|
0 = stop
|
|
P[]0 ~ P
|
|
P|||0 ~ P
|
|
P||0 ~ P
|
|
P[]Q ~ Q[]P
|
|
P|Q ~ Q|P valable pour ||, |||, |[]|
|
|
P[](Q[]R) ~ (P[]Q)[]R
|
|
P[]P ~ P
|
|
|
|
0 élément neutre pour [] (addition) et || (mult.)
|
|
<P,[],;> a une structure de monoïde.
|
|
|
|
a;(P[]Q) ~/ (a;P) [] (a;Q)
|
|
%Si on prend P:=b;0 et Q:=0, on a ". ->^a 0 ->^b -> 0" à gauche et . (/->^a 0) \->^a . ->^b 0
|
|
|
|
\end{document} |