MODEL CHECKING CON NUSMV

[Total: 0    Average: 0/5]

Un modo per verificare la correttezza e il buon funzionamento di un modello lo
si ottiene usando i metodi formali. Questi metodi di verifica si basano su due approcci principali: il primo consiste nel theorem proving automatico; il secondo invece, più recente, è quello del model
checking.
Nel primo caso, sia il sistema che le proprietà che si vogliono verificare devono
essere descritti in una logica appropriata. Viene poi costruita una dimostrazione del
fatto che la descrizione del sistema implica una descrizione della proprietà. Questo
approccio è molto flessibile e potente, ma, quanto più espressiva è la logica, tanto più risulta difficile costruire le dimostrazioni. Viene, quindi, richiesto spesso l’intervento
esterno dell’utente il quale deve suggerire lemmi, o passi intermedi di prova, affinché il
sistema riesca a suggerire una dimostrazione.
Nel secondo caso si necessita della descrizione del sistema sotto forma di
macchina a stati finiti e di proprietà espresse in una logica proposizionale temporale.
Viene poi usata un’efficiente procedura di ricerca per determinare in modo automatico,
se le specifiche sono soddisfatte dal grafo di transizione degli stati.