MODEL CHECKING CON NUSMV

Click to rate this post!
[Total: 1 Average: 4]

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 proporzionale 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.

0 0 votes
Article Rating
Subscribe
Notify of
guest

0 Comments
Inline Feedbacks
View all comments
0
Would love your thoughts, please comment.x
()
x