Strumento di controllo modello semplice

Question

Esiste un semplice strumento Model Checker. Ho in programma di implementare uno strumento di verifica dei modelli che analizzerà il codice per alcune delle proprietà predefinite.

Answer 1

Uno strumento importante è SPIN , con il linguaggio Promela. Se usi LaTeX, c'è anche TLA + .

Questi non analizzeranno il tuo codice, ma ti permetteranno di esprimere un modello per le tue assunzioni e i tuoi stati di transito, e quindi analizzeranno gli stati non validi. In altre parole, rileveranno problemi nel tuo modello, non nell'implementazione del tuo modello.

Ho visto una demo di Goanna , ma don ' non so se è disponibile (commerciale o altro); questo ha il vantaggio di analizzare effettivamente il tuo codice sorgente.

Solo guardando la tua domanda, e di nuovo i commenti nella tua domanda, sembra che dovresti davvero prima leggere un po 'di letteratura. Forse The Spin Model Checker o Specifica dei sistemi (scaricabile da sito Web di Leslie Lamport ). È necessario riformulare il problema in modo da non tentare di risolvere il problema di interruzione.

Answer 2

CBMC è uno strumento semplice di cui sono consapevole opera effettivamente sul codice. Il controllo del modello in generale è un campo molto ricercato, ma come la gente ha già commentato, questa ampiezza rende difficile suggerire qualcosa con le informazioni fornite. Esistono migliaia di solutori SAT, strumenti formali per la verifica delle macchine HDL / state e numerosi analizzatori di sorgenti statiche commerciali.

In ogni caso, CBMC è un buon strumento, ma non credetemi; Ed Clarke, il principale membro della facoltà dietro questo lavoro, ha vinto il Turing Award quest'anno ;-)