Model checking

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 $M,s \models p$.

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 real-time e forme limitate di sistemi ibridi.

Collegamenti esterni

Articoli

• (EN) An Introduction to Model Checking at embedded.com

Gruppi di ricerca

Italiani

• Model checking all'ITC-irst/Fondazione Kessler, Trento
• Artificial Intelligence Laboratory, Genova
• Model Checking al Dipartimento di Informatica, Universita' di Roma La Sapienza
• Formal Methods and Tools Lab - ISTI - CNR - Pisa’’
• EmbLab - Universita' di Modena e Reggio Emilia - Modena

Esteri

• Model Checking at Carnegie Mellon University
• SAnToS Laboratory at K-State
• Automated Software Engineering at Nasa Ames Research Center
• NASA/JPL Laboratory for Reliable Software
• VLSI/CAD Research group - University of Colorado at Boulder
• Verification and Validation - Brigham Young University, Provo, Utah
• ParaDiSe Laboratory - Masaryk University in Brno
• VASY Research team - INRIA Rhône-Alpes, France

Strumenti di model checking

• EmbeddedValidator, The Matlab/Simulink/Stateflow/TargetLink Formal Verification Environment
• Statemate ModelChecker, Statemate Models Robustness Checking
• Statemate ModelCertifier, Statemate Models Requirements Certification
• Alloy language
• APMC
• BLAST (Berkeley Lazy Abstraction Software Verification Tool)
• LoTREC
• Bogor
• BOOP Toolkit
• Charmy, CHARMY: A Framework for Designing and Verifying Architectural Specifications
• Cadena
• Cadence SMV
• CADP
• 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.
• HOL theorem prover
• Java Pathfinder
• MOPED
• MOPS, Modelchecking Programs for Security properties
• NuSMV: a new symbolic model checker
• Prism(model checker)
• ProB
• Probabilistic Symbolic Model Checker
• ProofPower
• PROSPER
• Rabbit
• RAVEN (Real-Time Analysis and Verification Environment)
• RuleBase
• SATABS, predicate abstraction for C/C++ programs
• SAL: Symbolic Analysis Laboratory
• SLAM project
• SMV: Symbolic Model Checker
• SPIN model checker
• UPPAAL - Uppaal Model Checker
• Verification Interacting with Synthesis (VIS)
• Database of Verification and Model Checking Tools (Yahoda)

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.

• Questa voce si basa su materiale disponibile sul Free On-line Dictionary of Computing (sito) e il suo utilizzo è regolamentato dalla licenza GFDL.