Groupe OLC
Outils et Logiciels pour la Communication

Projet
de
Recherche









Quizz RT-LOTOS

Christophe Lohr

1  Question

Précisez les dates des tirs des actions a, b, c du processus P suivant :
    P = hide a,b,c in Q[a,b,c] |[a,b,c]| R[a,b,c]

            Q[a,b,c] = delay(3,5) a; ( ( latency(10) b; stop )
                                       []
                                       ( c; stop ) )

            R[a,b,c] = a{8}; ( ( b; stop )
                               []
                               ( latency(10) c; stop ) )

Réponse en annexe A.

2  Question

Les processus P et Q sont-ils équivalents (bisimulation) ?
    P[a] = ( a{10}; exit ) [] ( delay(10) i; exit )

    Q[a] = ( a; exit ) [> ( delay(10) i; exit )

Réponse en annexe B.

3  Question

Proposez un processus RT-LOTOS équivalent au RdPT suivant :



Réponse en annexe C.

4  Question

Proposez un processus RT-LOTOS équivalent à l'AT suivant :



Réponse en annexe D.

5  Question

Proposez un processus RT-LOTOS équivalent au RdPT suivant :



[l] t1 = [2,5]
t2 = [3,8]
t3 = [0,+¥]
t4 = [1,4]

Réponse en annexe E.

6  Question

Donnez les dates possibles de tir des actions a, b et c spécifiées ainsi :
  specification Example : exit

  hide a, b, c in
   P[a,b,c] |[a,b,c]| Q[a,b,c]

  where
    process P[a,b,c] : exit :=
      (
        ( a{10}; exit )
        |||
        ( delay(5,10) b{5}; exit )
      )
      []
      (  delay(10) c !5; exit )
   endspec

   process Q[a,b,c] : exit :=
     ( latency(20) a; b; exit )
     []
     ( c !5; exit )
   endspec

Réponse en annexe F.

7  Question

Proposez un AT, puis un RdPT décrivant le comportement temporel global (date de tir des actions) spécifié par le code RT-LOTOS suivant :
  specification Example : exit

  hide a, b in
    P[a] |[a]| Q[a,b]

  where
    process P[a] : noexit :=
         delay(100) a{0}; P[a]
    endproc

    process Q[a,b] : noexit :=
         a; delay(10,20) b; Q[a,b]
    endproc

  endspec

Réponse en annexe G.

8  Question

On souhaite modéliser et évaluer le fonctionnement d'un document multimédia composé de deux Layers : audio et vidéo. Le comportement nominal d'un layer est caractérisé par deux actions open et close, et par trois contraintes temporelles : un temps de préchargement pendant lequel le layer est silencieux (appelé idle), une durée minimale de présentation (appelée dmin), et une durée maximale de présentation (appelée dmax).

Dans le cas du document étudié une contrainte supplémentaire a été ajoutée : l'audio et la vidéo doivent se terminer simultanément (action end_av).

Une modélisation en RT-LOTOS de ce système est proposée plus bas.

L'analyse d'accessibilité fait apparaître un ``dysfonctionnement'' (voir plus bas).
Q1 :
De quelle manière apparaît le dysfonctionnement ?
Q2 :
Quel concours de circonstance a amené le système à cette situation de dysfonctionnement ?
Réponse en annexe H.

Document multimédia : modélisation RT-LOTOS

   specification AudioVideo : noexit

   type natural is
      sorts nat
      opns
         +  : nat,nat->nat
         -  : nat,nat->nat
   endtype

   behaviour

     hide start_a, start_v, end_av in

     Layer[start_a,end_av](15,10,10)
     |[end_av]|
     Layer[start_v,end_av](5,15,20)

   where

     process Layer[open,close](idle,dmin,dmax:nat) : exit :=
       latency(idle) open{idle}; delay(dmin,dmax) close{dmax-dmin}; stop
     endproc

   endspec

Document multimédia : graphe de région

    0-(5 5) URG c1=5 c2=5 c2-c1=0 
    0-(0 0) 0<=c1<5 0<=c2<5 c2-c1=0 
    1-(5 5) URG 0<=c1<10 c2=5 -5<c2-c1<=5 
    1-(0 0) 0<=c1<10 0<=c2<5 -5<c2-c1<5 
    2-(15 15) URG c1=15 10<c2<=20 -5<c2-c1<=5 
    2-(15 10) URG c1=15 c2=10 c2-c1=-5 
    2-(0 0) 0<=c1<10 0<=c2<5 -5<c2-c1<5 
    2-(5 0) 5<=c1<10 0<=c2<5 c2-c1=-5 
    2-(5 5) 0<=c1<15 5<=c2<10 -5<c2-c1<=5 
    2-(10 5) 10<=c1<15 5<=c2<10 c2-c1=-5 
    2-(10 10) 5<=c1<15 c2=10 -5<c2-c1<=5 
    2-(10.5 10.5) 5<c1<15 10<c2<20 -5<c2-c1<=5 
    3-(10 20) URG c1=10 c2=20 c2-c1=10 
    3-(10 15) c1=10 15<=c2<20 5<=c2-c1<10 
    3-(10.5 10.5) c1>10 c2>=0 
    3-(5.5 20.5) 0<=c1<=10 c2>20 c2-c1>10 
    3-(0 0) 0<=c1<10 0<=c2<15 -10<c2-c1<5 
    3-(0 15) 0<=c1<10 10<c2<=20 10<c2-c1<=20 
    3-(0 5) 0<=c1<10 5<=c2<20 5<=c2-c1<10 
    3-(0 10) 0<=c1<10 10<=c2<20 c2-c1=10 
    3-(10 10) c1=10 0<=c2<15 -10<=c2-c1<5 
    4-() 
    ( 0-(5 5), i(start_a), 1-(5 5) )
    ( 0-(5 5), i(start_v), 2-(5 0) )
    ( 0-(0 0), i(start_a), 1-(0 0) )
    ( 0-(0 0), i(start_v), 2-(0 0) )
    ( 0-(0 0), t, 0-(5 5) )
    ( 1-(5 5), i(start_v), 3-(0 0) )
    ( 1-(0 0), i(start_v), 3-(0 0) )
    ( 1-(0 0), t, 1-(5 5) )
    ( 2-(15 15), i(start_a), 3-(0 15) )
    ( 2-(15 10), i(start_a), 3-(0 10) )
    ( 2-(0 0), i(start_a), 3-(0 0) )
    ( 2-(0 0), t, 2-(5 5) )
    ( 2-(5 0), i(start_a), 3-(0 0) )
    ( 2-(5 0), t, 2-(10 5) )
    ( 2-(5 5), i(start_a), 3-(0 5) )
    ( 2-(5 5), t, 2-(10 10) )
    ( 2-(10 5), i(start_a), 3-(0 5) )
    ( 2-(10 5), t, 2-(15 10) )
    ( 2-(10 10), i(start_a), 3-(0 10) )
    ( 2-(10 10), t, 2-(10.5 10.5) )
    ( 2-(10.5 10.5), i(start_a), 3-(0 15) )
    ( 2-(10.5 10.5), t, 2-(15 15) )
    ( 3-(10 20), i(end_av), 4-() )
    ( 3-(10 15), i(end_av), 4-() )
    ( 3-(10 15), t, 3-(10.5 10.5) )
    ( 3-(5.5 20.5), t, 3-(10.5 10.5) )
    ( 3-(0 0), t, 3-(10 10) )
    ( 3-(0 15), t, 3-(5.5 20.5) )
    ( 3-(0 5), t, 3-(10 15) )
    ( 3-(0 10), t, 3-(10 20) )
    ( 3-(10 10), t, 3-(10.5 10.5) )


A  Réponse à la question 1

a est tiré entre 3 et 5 unités de temps, puis, soit b, soit c, entre 0 et 10 unités de temps après le tir de a.

B  Réponse à la question 2

Oui ! L'action a est offerte pendant 10 unités de temps. Si le rendez-vous ne s'est pas produit, alors l'action i se produit.

C  Réponse à la question 3

hide t1,t2,t3 in P1

P1 = ( delay(2,5) t1; P2 ) [] ( delay(2,3) t2; P2 )
P2 = ( delay(1,2) t3; P1 )

D  Réponse à la question 4

hide a, b in  P1[a] |[a]| P2[a,b]

P1[a] = delay(20) a{0}; P1[a]
P2[a,b] = a; delay(5,10) b; P2[a,b]

E  Réponse à la question 5

hide t1,t2,t3 in A

A = delay(2,5) t1; ( (delay(3,8) t2; B) ||| (delay(1,4) t4; B) )
                        >> ( B [] A )
B = t3; stop

F  Réponse à la question 6

Soit a entre 0 et 10 suivie de b, ou alors c entre 0 et 10, avec échange de la valeur 5.

G  Réponse à la question 7





H  Réponse à la question 8

R1 :
Le noeud 3-(10.5 10.5) du graphe d'accessiblité n'a pas de transition de sortie alors que le système devrait se terminer par l'action end_av
R2 :
Le système démarre le layer audio trop tard pour que les deux layers puissent synchroniser leur terminaison.

 Retour au projet RT-LOTOS

Ce document a été traduit de LATEX par HEVEA.