Definizione e caratteristiche della tecnica del Model Checking in informatica

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

Definizione e caratteristiche della tecnica del Model Checking in informatica

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

  1. 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;
  2. specifica di  un  insieme  di  proprietà  mediante  logiche temporali (quale LTL o CTL), formulate su attributi del modello definito precedentemente;
  3. 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.

Precedente Obiettivi e vantaggi di utilizzo dei portali aziendali (Enterprice Portals) Successivo La visione artificiale a supporto della videosorveglianza

Lascia un commento

*