model checking

In breve:Esistono decine di software per il model checking, ciascuno specializzato in determinati modelli, linguaggi o domini. I più noti includono SPIN, NuSMV, PRISM e UPPAAL. Cos’è il model checking Il model checking è una tecnica automatica di verifica formale usata per controllare se un modello di sistema soddisfa specifiche proprietà logiche. Viene impiegato soprattutto per rilevare errori in sistemi software o hardware complessi. Come funziona Il model checking confronta un modello formale del sistema con una specifica data, espressa in logica temporale.Processo tipico: Il sistema viene modellato come macchina a stati finiti Le proprietà da verificare sono espresse formalmente…