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 Alloy (Analizzatore di leghe) BLAST (Berkeley Lazy Abstraction Software Verification Tool) CADP CPAchecker: ECLAIR: FDR2: ISP Java Pathfinder: un modello open-source per programmi Java Libdmc: un framework per il model checking distribuito mCRL2 Insieme di strumenti, Boost Software License, basato sull'algebra ACP NuSMV: PAT: Prism: un model checker simbolico probabilstico Roméo: un ambiente integrato per la modellazione, validazione e verifica di sistemi in tempo reale modellati in maniera parametrica, sul tempo, e su Reti di Petri stopwatch SPIN: TAPAs: TAPAAL: un ambiente integrato per la modellazione, validazione e verifica di Reti di Petri Timed-Arc TLA+ model checker di Leslie Lamport UPPAAL:
Bibliografia Model Checking , Doron Peled, Patrizio Pelliccione, Paola Spoletini, Wiley Encyclopedia of Computer Science and Engineering, 2009. Promela and SPIN: What do they promise?, Venkatesh Vinayakarao, 2006. Automatic verification of finite state concurrent systems using temporal logic, E.M. Clarke, E.A. Emerson, and A.P. Sistla, ACM Trans. on Programming Languages and Systems, 8(2), pp. 244–263, 1986. Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press, 1999. Concurrency theory, calculi and automata for modelling untimed and timed concurrent systems, H. Bowman and R.S. Gomez. Springer, January 2006.
Altri progetti
Collegamenti esterni
Articoli at embedded.com
Gruppi di ricerca
Model Checking al Dipartimento di Informatica, Università di Roma La Sapienza
Strumenti di model checking
BLAST (Berkeley Lazy Abstraction Software Verification Tool)
BOOP Toolkit
Cadena Cadence SMV
CBMC, a bounded Model Checker for C/C++ programs CHIC CMurphi Caching Murphi COSPAN Coverity Goanna static code analysis via model checking. GEAR, a game based model checking tool capable of CTL, modal μ-calculus and specification patterns.
MOPS, Modelchecking Programs for Security properties
:Prism(model checker)
Probabilistic Symbolic Model Checker ProofPower PROSPER Rabbit
SATABS, predicate abstraction for C/C++ programs
SLAM project
Database of Verification and Model Checking Tools (Yahoda)
Categoria:Logica nell'informatica Categoria:Metodi formali Categoria:Ragionamento automatico