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 lintervento esterno dellutente 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 unefficiente procedura di ricerca per determinare in modo automatico, se le specifiche sono soddisfatte dal grafo di transizione degli stati.
