Introduzione a un Linguaggio logico di specifica delle proprietà
Elementi essenziali
Il sistema da verificare è descritto da un LTS ;
Le asserzioni elementari sono espresse da un insieme AP di proposizioni atomiche;
Gli stati dell’LTS sono decorati con un insieme di proposizioni atomiche mediante una funzione
Se l’asserzione p vale nello stato s;
Se l’asserzione p non vale nello stato s.
La struttura che ne deriva è chiamata struttura di Kripke ed ha la forma .
LTS di un arbitro che soddisfa le richieste di accesso ad una risorsa condivisa per due processi richiedenti.
Alfabeto transizioni:
(richiesta dell’iesimo processo)
(assegnazione all’iesimo processo)
(rilascio dell’i-esimo processo)
Proposizioni atomiche:
(iesimo processo inattivo)
(iesimo processo in attesa)
(i-esimo processo con risorsa assegnata)
Un cammino della struttura di Kripke K è la struttura su cui viene valutata una formula di LTL.
Un cammino è un comportamento dell’LTS (specifica del sistema);
Un cammino è una sequenza di insiemi di proposizioni atomiche;
La formula descrive una proprietà del sistema di cui si vuole verificare il soddisfacimento.
Esempio di cammino (si omettono gli archi delle transizioni):
Il cammino considerato soddisfa la seguente proprietà (informale):
Se il processo 1 è in stato di attesa, successivamente avrà assegnata la risorsa.
Model checking
La struttura di Kripke K verifica la proprietà () se ogni cammino di K (a partire dallo stato iniziale) è un modello per la proprietà.
Il modello di Kripke verifica la seguente proprietà (informale).
Per ogni stato, se il processo 1 è in stato di attesa ( è vera), nello stato successivo avrà assegnata la risorsa ( è vera).
Il modello di Kripke non verifica la seguente proprietà (informale).
Esiste un punto della computazione in cui il processo 1 avrà assegnata la risorsa.
La proprietà non è verificata perché il cammino che attraversa ciclicamente i soli stati non soddisfa la proprietà.
Insieme AP di proposizioni atomiche
Formule
Il soddisfacimento di una formula è valutato rispetto ad una sequenza (infinita) :
Sequenza infinita di sottoinsiemi di AP;
E’ la sequenza di etichette associati agli stati di un cammino iniziale di una struttura di Kripke.
Notazione:
indica il sottoinsieme di AP associato all’i-esima posizione della sequenza
(insieme di proposizioni atomiche vere nell’i-esimo stato del cammino della struttura di kripke).
Ogni formula è valutata in un punto specifico della sequenza
Operatore temporale NEXT (Successore)
Operatore temporale Future (Nel futuro si verifica la proprietà)
Operatore temporale Globally (la proprietà si verifica sempre)
Uno dei due processi è sempre inattivo
Dopo aver raggiunto lo stato di attesa si accede in un passo alla risorsa
Operatore temporale Untile (nel futuro deve valere e nel frattempo deve valere con continuità )
Il secondo process sarà ad un certo punto in attesa e nel frattempo è inattivo.
Connettivi standard derivati:
True è abbreviazione per
per qualche
È abbreviazione per
È abbreviazione per
Operatori temporali derivati:
è abbreviazione per
è abbreviazione per
Altri operatori temporali:
(Before)
non può essere osservato senza che prima sia osservato
È esprimibile con
Altri operatori temporali:
(Unless)
Sempre a meno che non si osservi
È esprimibile con
Si osservi che È esprimibile con
Altri operatori temporali:
(Releases)
Sempre a meno che non si osservi prima
È esprimibile con
Si osservi che Releases è l’operatore duale di Until
Sia una struttura di Kripke e una formula di LTL.
Un AP-cammino di K è una sequenza
Dove sono la sequenza di stati di un comportamento originato dallo stato iniziale.
(sequenza di insiemi di proposizioni atomiche che etichettano un comportamento dell’LTS)
(problema del model checking)
Se per ogni AP-cammino vale che .
Non può mai capitare che entrambi i processi possano avere la risorsa allo stesso tempo
Se in stato di attesa avrà la risorsa
Ogni processo è infinitamente spesso inattivo
Ogni processo se è infinitamente spesso in attesa, infinitamente spesso avrà la risorsa
Non vale però
1. Introduzione ai metodi formali di specifica
2. Semantica dei formalismi di specifica
3. Astrazione e Bisimulazione debole
4. FSM: Macchine a Stati Finiti
5. FSM: Non-determinismo e succintezza
7. FSM e Parallelismo – seconda parte
8. FSM e Parallelismo – terza parte
9. Promela
10. Specifica e verifica in SPIN
11. Proprietà di liveness in SPIN
12. Specifica di proprietà in Logica Temporale Lineare
13. Comportamenti infiniti: Automi di Büchi
14. Model checking di LTL basato su automi
15. Specifica di sistemi real time: Automi Temporizzati
16. Proprietà degli Automi Temporizzati
17. Problemi di decisione negli Automi Temporizzati
18. Il sistema di verifica UPPAAL