Il model checking è un metodo per verificare algoritmicamente i sistemi formali. Viene realizzato mediante la verifica del modello, spesso derivato dal modello hardware o software, soddisfacendo una specifica formale. La specifica è spesso scritta come formule logiche temporali.

Il modello solitamente viene espresso come un sistema di transizioni, cioè grafo orientato formato da nodi (o vertici) e archi. Un insieme di proposizioni atomiche è associato ad ogni nodo. I nodi rappresentano gli stati di un sistema, gli archi rappresentano le possibili esecuzioni che alterino lo stato, mentre le proposizioni atomiche rappresentano le proprietà fondamentali che caratterizzano un punto di esecuzione.

Formalmente il problema è posto così: scelta una proprietà da verificare, espressa come una formula logica temporale p, e un modello M avente stato iniziale s, decidere se .

Gli strumenti del model checking si scontrano con la crescita esponenziale dell'insieme degli stati, comunemente conosciuto come il problema dell'esplosione combinatoria, che deve servire a risolvere la maggior parte dei problemi del mondo reale. I ricercatori hanno sviluppato algoritmi simbolici, riduzione parziale dell'ordine, diagrammi decisionali, astrazioni e model checking al volo per risolvere il problema. Questi strumenti furono inizialmente sviluppati per la correttezza logica dei sistemi a stati discreti, ma da allora sono stati estesi per trattare sistemi sistema real-time e forme limitate di sistemi ibridi.

Strumenti modifica

Bibliografia modifica

Voci correlate modifica

Altri progetti modifica

Collegamenti esterni modifica

Articoli modifica

  • (EN) An Introduction to Model Checking[collegamento interrotto] at embedded.com

Gruppi di ricerca modifica

Strumenti di model checking modifica

  Portale Informatica: accedi alle voci di Wikipedia che trattano di informatica