La forma di comunicazione tra le componenti è quella elementare della condivisione di variabili.
La forma di comunicazione è classificabile come:
Per semplicità si assume:
La limitazione sui valori delle variabili è essenziale per garantire la finitezza degli stati del sistema.
Nella forma più generale, una transizione di una macchina a stato-transizione assume la forma
Nel formalismo preso in considerazione si ha che:
Il Trigger mantiene la forma semplice di uno simbolo appartenente ad un alfabeto;
La Condizione è una espressione booleana sul contenuto delle variabili in Var;
l’Azione è un insieme di assegnazioni di una espressione aritmetica ad una variabile.
Categoria delle espressioni aritmetiche Aexp
La categoria Aexp delle espressioni aritmetiche sull’inseme delle variabili Var è definita come segue:
dove .
Categoria delle espressioni booleane Bexp
La categoria Bexp delle espressioni booleane sull’insieme delle variabili Var è definita come segue:
dove .
Categoria delle assegnazioni Assign
La categoria Assign delle assegnazioni è definita dall’insieme delle espressioni della forma
.
Fissato un insieme Var di variabili intere un automa parallelo ha la forma
Si assume che se in A non possano comparire due assegnazioni alla stessa variabile.
La descrizione dello stato globale di un automa comprende lo stato di controllo di ciascuna delle componenti e la valutazione delle variabili in Var.
La valutazione delle variabili Var è descritta da una funzione (totale) di valutazione
tale che .
Sia l’insieme delle possibili funzioni di valutazione delle variabili.
La semantica è data dall’LTS
con .
Preliminare alla definizione della relazione di transizione dell’LTS è la definizione della valutazione di espressioni aritmetiche e booleane.
Per una espressione , la funzione di valutazione
è definita induttivamente come segue:
Per una espressione , la funzione di valutazione
è definita induttivamente come segue:
è data dal seguente insieme di transizioni:
Il modello di parallelismo adottato è puramente interleaving (scatta una sola transizione alla volta).
Si osservi che l’assegnazione delle variabili devono rispettare i limiti MinInt e MaxInt del dominio di definizione.
Il mancato rispetto ha effetto bloccante sulla transizione.
Soluzione 1.
Soluzione 2.
Formulazione 1:
Non garantisce la mutua esclusione nell’accesso alla sezione critica.
Nell’entrata nella sezione critica il controllo di flag2 e l’assegnazione di flag1 non sono atomiche e separabili dall’interfogliazione nell’esecuzione delle transizioni.
Formulazione 2:
Garantisce la mutua esclusione nell’accesso alla sezione critica.
Nell’entrata nella sezione critica il controllo di flag2 e l’assegnazione di flag1 sono atomiche (sono fatte nella medesima transizione).
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