Definizione e caratteristiche della tecnica del Model Checking in informatica
Introduzione al model checking
La progettazione di sistemi software sempre più complessi ha visto recentemente uno sviluppo di diversi approcci alla progettazione stessa. Tra di essi, un approccio diffuso è quello guidato dalla definizione di un modello del sistema considerato utilizzando notazioni formali (FSM, Z, logiche) o semi formali (UML) per valutare proprietà del sistema prima della sua effetiva implementazione. A supporto di tale attività, il model checking è una tecnica di verifica automatica che consente di definire un modello del sistema con una notazione formale,specificare in logica temporale le proprietà desiderate e verificare quest’ultime. A tal proposito, il model checking è una tecnica molto potente e molto utilizzata per lo sviluppo di sistemi critici anche se non ampiamente utilizzata altrove per alcune problematicità citate qui di seguito.
Caratteristiche del model checking
Una metodologia adottata in diversi contesti per la progettazione di un sistema software, è quella cosiddetta model driven, ossia uno sviluppo del software guidato dalla definizione di un modello del sistema software stesso. La definizione di un modello consente di disporre di una descrizione delle caratteristiche salienti del sistema senza occuparsi degli aspetti implementativi; in fase di progetto è utile poter riflettere su tali caratteristiche, se esse soddisfano i requisiti richiesti o se vanno modificate: il vantaggio è quello di poter manipolare un modello astratto anzichè dover implementare un sistema per poi scoprire che contiene errori che richiedono la riprogettazione dell’intero sistema o di alcune sue parti. Inoltre, nello sviluppo di sistemi software in cui si utilizzano componenti costosi, effettuare test o simulazioni sul sistema reale potrebbe essere costoso o addirittura potrebbe essere meglio ragionare su un modello del sistema per cercare di comprendere che tipo di componenti scegliere e con quale architettura comporre tali componenti. A supporto di questa fase di riflessione sulle caratteristiche del modello il model checking consente di definire un modello con un formalismo (strutture di Kripke) e successivamente verificare proprietà del modello rispetto a specifiche formulate tramite logiche temporali; come vedremo successivamente, il model checking offre diversi vantaggi quali la definizione di un modello formale del sistema assai aderente alla successiva implementazione, la possibilità di specificare proprietà del sistema mediante logiche temporali, la dimostrazione della validità di tali proprietà rispetto al modello e infine la disponibilità di un modello eseguibile ossia di un modello su cui si possono effettuare simulazioni.
Utilizzo pratico del model checking
Utilizzando il model checking è possibile supportare dunque lo sviluppo di un sistema software con una procedura che parte dalla definizione di un modello del sistema per individuarne meglio le caratteristiche salienti senza dover subito occuparsi degli aspetti implementativi, specificare delle proprietà in modo rigoroso con logiche temporali e infine verificare tali proprietà allo scopo di cercare di dimostrarne la validità o di identificare errori nelle scelte progettuali; più precisamente la procedura con cui viene effettuata l’attività di
- definizione di un modello formale del sistema in via di sviluppo; per il model checking il formalismo utilizzatoè in generale definito mediante strutture di Kripke, una sorta di macchine a stati finiti;
- specifica di un insieme di proprietà mediante logiche temporali (quale LTL o CTL), formulate su attributi del modello definito precedentemente;
- esecuzione di verifica automatica delle proprietà definite al punto 2 mediante strumenti che implementano tale verifica; a titolo di esempio, verifichiamo alcune proprietà utilizzando due strumenti, ad esempio Spin e NuSMV, che tra le loro funzionalità comprendono la verifica automatica anche se non entreremo nei dettagli degli algoritmi di verifica dei due model checker per non complicare eccessivamente la panoramica sul model checking.
