Model Checking¶
Lezione del 2019-01-24
Il model checking è l’alternativa alla equivalence checking nel fare la verifica della modellazione del sistema.
Come equivalence checking in questo corso si è visto in particolare l’uso della bisimulazione.
E' necessario considerare il fatto che, prese nella loro accezione più
generale, i controlli di equivalenza appartengono alla classe dei problemi
non decidibili. Questo vale per la programmazione sequenziale, ma anche per
l’algebra di processi se non si impone la limitazione dello studio di
sistemi che originano modelli finiti.
Avendo a che fare con problemi in generale indecidibili, si può decidere di fare ricorso a metodologie di test.
Queste metodologie impongono un cambio di paradigma. Un test verifica il comportamento del sistema in un particolare caso, confrontandolo con un risultato atteso. Se il riscontro è positivo il test ha dimostrato il corretto funzionamento del sistema … in quel caso.
Se un sistema può gestire un numero infinito di casi, per dimostrare in toto il suo corretto funzionamento dovremmo applicare infiniti test. E per farlo avremmo bisogno di una infinita quantità di tempo.
Il model checking è simile al testing. A differenza della bisimulazione, che controlla tutta la descrizione del sistema, confrontandola con un’altra di riferimento, il model checking verifica se una particolare proprietà é soddisfatta dal nostro sistema.
Dato un sistema scritto con un qualunque linguaggio formale di specifica [1], possiamo modellarlo con un labeled transition system. A questo punto consideriamo una sua proprietà.
Ad esempio, data una coffee machine, vogliamo verificare la proprietà: «eroga la bevanda solo dopo avere acquisito il pagamento?».
Per esprimere la proprietà da verificare si usa una formula \(\varphi\) che lo esprime tramite un linguaggio formale \(\mathbb{L}\).
Il model checking è l’algoritmo che verifica se il modello LTS soddisfa la formula \(\varphi\) predetta.
In generale il processo di progettazione si svolgerà come segue.
Descriveremo le specifiche del sistema tramite un linguaggio formale di specifica, ad esempio CCS.
Applicando la semantica operazionale alla specifica, genereremo (automaticamente) il modello LTS del nostro sistema.
Dato il linguaggio \(\mathbb{L}\) per esprimere le proprietà del modello [2], ad esempio una context free grammar come segue:
gli elementi del linguaggio sono:
- il terminale true,
- l’operatore di negazione: \(\neg\varphi\),
- l’operatore di congiunzione: \(\varphi\wedge\varphi\),
- l’operatore diamond \(<\!\mu\!>\cdot\varphi\), dove \(\varphi\) è una azione visibile o invisibile (\(\varphi\in Act_\tau\)).
Intuitivamente, avremo il seguente comportamento. Un algoritmo per verificare la formula \(\varphi\) rispetto uno stato dello LTS, valuterà se \(\varphi\) è soddisfatta dallo stato in analisi:
- se soddisfatta vale true;
- se vale \(\neg true\), allora è soddisfatta \(\neg\varphi\);
- se valgono true sia \(\varphi_1\) che \(\varphi_2\), allora vale true anche \(\varphi_1\wedge\varphi_2\);
- se esiste uno stato in grado di eseguire \(\mu\) andando in uno stato successivo in cui \(\varphi\) che sia true, allora lo è \(<\!\mu\!>\cdot\varphi\).
Formalmente, «uno stato s soddisfa la formula \(\varphi\) del linguaggio \(\mathbb{L}\) (ovvero: \(s \vDash \varphi \in \mathbb{L}\)) se e solo se valgono le seguenti regole induttive su \(\varphi\)»:
- \(s \vDash true\), vale sempre;
- \(s \vDash \neg \varphi\) se \(s \vDash true\) è false;
- \(s \vDash \varphi_1 \wedge \varphi_2\) se \(s \vDash \varphi_1\) e \(s \vDash \varphi_2\);
- \(s \vDash <\!\mu\!> \cdot \varphi\) se \(s \xrightarrow{\mu} s'\) e \(s' \vDash \varphi\);
Si può usare De Morgan per definire il false, l’operatore di disgiunzione, e così via. In particolare:
- il next\(\varphi\) definito come:
- \(s \vDash X_\varphi\) se \(s \xrightarrow{\mu} s'\) e \(s' \vDash \varphi\) per qualunque \(\mu \in Act_\tau\) [3];
- e lo until\(\varphi\) come segue:
- \(s \vDash \cup_\varphi\) se \(s \xrightarrow{\mu_1} \cdots \xrightarrow{\mu_n} s'\) tale che \(s' \vDash \varphi\) e \(\mu_1 \cdots \mu_n \in Act_\tau\) [4].
Esiste un teorema che afferma: «dati i processi P e Q espressi in CCS, questi sono bisimili se e solo se per ogni \(\varphi\) in \(\mathbb{L}\) avviene che P soddisfa \(\varphi\) se e solo se Q soddisfa \(\varphi\)»:
intuitivamente: due processi sono equivalenti se e solo se soddisfano lo stesso set di casi di prova.
| [1] | R.E., CCS, CSP, LOTOS, … |
| [2] | Tipicamente questi sono linguaggi logici. |
| [3] | Ovvero lo stato s soddisfa l’attributo \(\varphi\) dopo avere raggiunto un altro stato \(s'\) tramite una qualunque azione. |
| [4] | In questo caso, intuitivamente, raggiungo uno stato che soddisfa \(\varphi\) con una sequenza di azioni. |