Home

Federica EU

1/18

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.

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.

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.

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.