Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

Adriano Peron » 19.Verifica di proprietà in UPPAAL


Temi della lezione

La logica tempororale CTL (Computation Tree Logic)

  • Modello temporale branching
  • Sintassi
  • Semantica

Descrizione del linguaggio di specifica delle proprietà in UPPAAL

  • Raggiungibilità
  • Safety
  • Liveness

Esempi di proprietà: il caso dell’accesso dei treni al ponte.

Linguaggio di specifica di proprietà

Come linguaggio di specifica di proprietà UPPAAL usa un frammento della logica temporale CTL (Computation Tree Logic).

LTL vs CTL

LTL

LTL adotta un modello del tempo lineare.
I modelli sono sequenze lineari infinite: cammini in una struttura di Kripke.
Una formula di LTL predica delle proprietà di una sola computazione (sequenza lineare di stati associati alla computazione).
Non consente di esprimere proprietà che coinvolgano i percorsi alternativi che sono possibili per una scelta operabile in punto della computazione.

CTL

LTL adotta un modello del tempo ramificato (branching).
I modelli sono alberi ottenuti dallo ’srotolamento’ (unwind) di una struttura di Kripke.
Una formula di CTL può predicare di proprietà che coinvolgono simultaneamente possibili computazioni originate da un comune stato di partenza (computazioni alternative).

Tempo lineare vs tempo ramificato (branching)


Unwind della struttura di kripke dallo stato s_0

Sia K=\langle S_0,S,\Delta, L \rangle una struttura di Kripke.

TR(K,s)=\langle \{(s,\epsilon)\},  S_s,\Delta_s,L_s \rangle detto albero di computazione radicato nello stato s\in S è l’albero ottenuto ’srotolando’ K a partire dallo stato s (tutte le possibili computazioni a partire da s).

E’ definito induttivamente come segue:

S_s \subseteq S \times S^{\star}
(s,\epsilon) \in S_s
(s_1,\sigma) \in S_s \mbox{ e } (s_1,a,s_2) \in \Delta \mbox{ implica } (s_2,\sigma\cdot s_1) \in S_s \mbox{ e } ((s_1,\sigma),a,(s_2,\sigma\cdot s_1)) \in \Delta_s
L_s((s_1,\sigma))=L(s) \mbox{ per ogni } (s_1,\sigma)\in S_s

Si osserva che uno stato (s_1,\sigma)\in S_s rappresenta il fatto che dallo stato s in K si raggiunge lo stato s_1 con una sequenza di stati \sigma

TR(K,s) è di fatto una struttura di Kripke strutturata ad albero.

Esempio di unwinding


Sintassi di CTL

Sia AP un insieme di proposizioni atomiche

La sintassi di CTL è definita come segue:

\phi ::= True\ \mid\ p\ \mid\ \neg \phi\ \mid\ \phi \vee \phi\ \mid\ \phi \wedge \phi\ \mid\ EX\ \phi\ \mid\ EU(\phi, \phi)\ \mid\ AU(\phi, \phi)

con p\in AP.

Intuizione operatori temporali

EX\ \phi esiste uno stato successore dello stato corrente dove è verificata \phi
EU(\phi_1, \phi_2) esiste un cammino a partire dallo stato corrente dove è soddisfatta \phi_1\ U\ \phi_2
AU(\phi_1, \phi_2) per ogni cammino che parte dallo stato corrente è soddisfatta \phi_1\ U\ \phi_2

Semantica di CTL

Sia K=\langle S_0,S,\Delta,L\rangle una struttura di Kripke, s\in S e \phi una formula di CTL.

K,s \models \phi \mbox{ se e solo se } TR(K,s),(s,\epsilon) \models \phi

K,s \models\ True

K,s \models p \mbox{ se e solo se } p\in L(s)

K,s \models \phi_1 \wedge \phi_2 \mbox{ se e solo se } K,s \models \phi_1 \mbox{ e } K,s \models \phi_2

K,s \models \phi_1 \vee \phi_2 \mbox{ se e solo se } K,s \models \phi_1 \mbox{ o } K,s \models \phi_2

K,s \models \neg \phi \mbox{ se e solo se non vale che } K,s \models \phi

Semantica CTL: operatore EX

K=\langle S_0,S,\Delta,L\rangle

K,s \models EX\ \phi se e solo se esiste (s,a,s') \in \Delta \mbox{ e } K,s' \models \phi

Con riferimento a TR(K,s_0) in figura:

TR(K,s_0),(s_0,\epsilon)\models w_1
TR(K,s_0),(s_0,s_0\cdot s_1\cdot s_2)\models\ EX\  w_1
TR(K,s_0),(s_0,\epsilon)\models\  EX\ w_2
TR(K,s_0),(s_0,\epsilon)\not\models\ EX\ w_1\wedge w_2

Fig. 3. Semantica EX.

Fig. 3. Semantica EX.


Semantica CTL: operatore EU

K=\langle S_0,S,\Delta,L\rangle
K,s \models EU (\phi_1,\phi_2) se e solo se esiste un cammino di K
\pi=s_0,s_1,\ldots \mbox{ con } s_0=s ed esiste i\geq 0 tale che:
K,s_i \models \phi_2
K,s_j \models \phi_1 \mbox{ per ogni }  0\leq j < i

Con riferimento a TR(K,s_0) in figura:
TR(K,s_0),(s_0,\epsilon)\models EU(r_1,w_1)
TR(K,s_0),(s_0,\epsilon)\models EU(r_2,w_2)
TR(K,s_0),(s_0,\epsilon)\models \neg EU(True,\neg r_1\wedge \neg r_2)
(in ogni stato vale r_1\vee r_2)

Fig. 4. Semantica EU.

Fig. 4. Semantica EU.


Semantica CTL: operatore AU

K=\langle S_0,S,\Delta,L\rangle

K,s \models AU (\phi_1,\phi_2) se e solo se pero ogni cammino di K
\pi=s_0,s_1,\ldots \mbox{ con } s_0=s esiste i\geq 0 tale che:
K,s_i \models \phi_2
K,s_j \models \phi_1 \mbox{ per ogni }  0\leq j < i

Con riferimento a TR(K,s_0) in figura:

TR(K,s_0),(s_0,\epsilon)\models AU(True,EU(True,w_1))

In ogni cammino si diparte un cammino dove nel futuro w_1 è vera.

Fig. 5. Semantica AU.

Fig. 5. Semantica AU.


CTL e UPPAAL

UPPAAL usa una versione semplificata di CTL

Non viene permesso l’innesto di formule di cammino (AU e EU) all’interno di formule di cammino.

UPPAL suddivide le formule per l’espressione delle proprietà in

Formule di stato (state formulae)
Sono espressioni che possono essere valutate su uno stato senza guardare al comportamento del sistema (essenzialmente una combinazione booleana di proposizioni atomiche).

Formule di cammino (path formulae)
Espressioni che debbono essere valutate su un albero delle computazioni per la presenza di operatori temporali (tra loro non innestati)

Sono classificate in

  • formule di raggiungibilità (reachability formulae);
  • formule di safety;
  • formule di liveness.

UPPAAL: formule di stato

Rispetto a CTL possono essere viste come una combinazione booleana di proposizioni atomiche.

Sono un sovrainsieme delle formule che possono comparire nelle guardie delle transizioni.

Le proposizioni atomiche comprendono:

  • condizioni sul contenuto delle variabili (Es. I==7);
  • condizioni sull’avanzamento del controllo (Es. P.l è vera quando il proceso P si trova nella locazione l);
  • la proposizione deadlock che vale in tutti gli stati dove non esiste alcuna transizione uscente (a rigore sarebbe una formula di comportamento e non di stato);
  • sono ammesse le combinazioni booleane libere con gli operatori \wedge, \vee, \neg.

UPPAAL: formule di cammino

Proprietà di raggiungibilità

Esiste un cammino (una computazione) che raggiunge uno stato dove è soddisfatta la formula di stato \phi

Formula in UPPAAL

E<> \ \phi

Corrispondente formula di CTL

EU(True, \phi)

Limitazioni rispetto a CTL:
La formula \phi è una formula di stato che non può contenere nidificazione di altre formule temporali
Ha la forma ristretta di un operatore Eventually e non la piena espressività di un operatore Until.

UPPAAL: formule di cammino (segue)

Proprietà di safety

Nulla di negativo può mai capitare.
La proprietà viene di solito espressa in termini positivi secondo due modalità:

(1) Una proprietà di stato \phi vale in tutti gli stati raggiungibili

A[] \ \phi

Corrispondente formula di CTL

\neg EU(True, \neg\phi)

(2) Esiste un cammino massimale dove una proprietà di stato \phi vale in tutti gli stati.

E[] \ \phi

UPPAAL: formule di cammino (segue)

Proprietà di liveness

Qualche cosa di desiderato alla fine capita.
La proprietà ha due modalità di espressione:

(1) Una proprietà di stato \phi viene alla fine soddisfatta in tutti i cammini

A<> \ \phi

Corrispondente formula di CTL

AU(True, \phi)

(2) Quando \phi è soddisfatta alla fine \psi sarà soddisfatta.

\phi --> \psi

Corrispondente formula di CTL

AU(\neg \phi, \phi\wedge\ EU(True,\psi))

Proprietà per il treno e per il controller del ponte


Esempi di proprietà per treno e ponte

Raggiungibilità

Il controllore del ponte riceve e memorizza messaggi di treni che si approssimano al ponte

E<>\ Gate.Occ

Il treno 1 può attraversare il ponte prima o poi

E<>\ Train1.Cross

Il treno 1 attraversa il ponte e gli altri tre treni rimangono in attesa

E<>\ Train1.Cross\ and\ Train2.Stop\ and\ Train3.Stop\ and\ Train4.stop

Gli esempi di proprietà riportati garantiscono solo la raggiungibilità di stati dove la proprietà di stato è verificata; ad esempio non garantiscono che sempre i treni accedano al ponte in mutua esclusione.

Esempi di proprietà per treno e ponte (segue)

Safety

Non ci può essere più di un treno alla volta che attraversa il ponte

A[]\ Train1.Cross+Train2.Cross+Train3.Cross+Train4.Cross<=1

(l’espressione sfrutta il fatto che i valori booleani sono 0,1)

La coda non raggiunge mai l’overflow

A[]\ (Gate.Free\ or\ Gate.Occ)\ implies\ Queue.len < N-1

(N è fissato come numero dei treni + 1; Free e Occ sono i soli due stati in cui si può fare una operazione di enqueue)

Liveness

Se il treno si avvicina al ponte alla fine lo attraversa

Train1.Appr -->Train1.Cross

Il sistema non incorre in fenomeni di stallo

A[]\ not\ deadlock

  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion