Un sistema reattivo è un sistema (in genere concorrente) che interagisce con l'ambiente in cui opera. Cioè un sistema reattivo reagisce all'input (dall'ambiente) producendo un output (verso l'ambiente) e cambiando il suo stato interno.
Dal punto di vista funzionale un sistema reattivo è costituito da un insieme di componenti hardware e/o software, che collaborano e si condizionano per raggiungere uno scopo presfissato.
Ecco alcuni esempi di sistemi reattivi: Sistemi Embedded , SOC (Systems On Chip) , Sistemi Operativi , Protocolli , Sistemi di Controllo, Hardware Digitale, Sistemi Ibridi (cioè sistemi dinamici nei quali lo stato ha sia componenti discrete che componenti continue).
Sistemi reattivi sempre più complessi sono oggi usati nell'elaborazione distribuita; nelle telecomunicazioni; nel controllo di impianti industriali; nei sistemi embedded su automobili, treni, aerei, elettrodomestici (consumer electronics), etc.
La progettazione di sistemi reattivi avviene con un time-to-market sempre più corto e/o con un costo degli errori sempre più alto. Questo tende a far crescere sempre più il costo della fase di testing per tali sistemi. Il costo del testing nel progetto di sistemi reattivi oggi è tipicamente nell'ordine del 50% del costo totale.
D'altro canto bisonga tenere presente che gli errori progettuali aumentano il tempo necessario alla completazione del progetto e quindi aumentano il costo finale del progetto stesso. Inoltre gli errori progettuali aumentano il time-to-market. A causa del ciclo di vita corto di molti sistemi reattivi (e.g. consumer electronics) questo si traduce in mancati guadagni e perdite di market share.
Infine bisonga tenere presente che più tardi un errore viene rilevato nel ciclo progettuale, maggiore è il costo (economico e temporale) della sua correzione.
La situazione delineata sopra rende sempre più acuto il bisogno di rilevare gli errori progettuali il più presto possibile nel ciclo progettuale, con l'obiettivo di rilasciare nel più breve tempo possibile un prodotto di elevata qualità (bug free).
L'obiettivo principale della ricerca sui metodi di analisi automatica di sistemi reattivi è appunto quello di rilevare gli errori progettuali il più presto possibile nel ciclo progettuale. Questo riduce l'attività di debugging, riduce il costo del prodotto finale, riduce il time-to-market ed, infine, aumenta la qualità del prodotto finale. Di fatto evitare che l'attività di debugging cresca oltre il 50% del costo finale è già un obiettivo al momento spesso difficile da raggiungere.
La verifica automatica affianca il testing e la simulazione nell'analisi di un sistema. La differenza fondamentale è che il testing e la simulazione considerano solo alcune delle possibili evoluzioni di un sistema. La verifica automatica, invece, considera tutte le possibili evoluzioni del sistema.
Testing e simulazione hanno una basso costo computazionale, ma conducono un'analisi approssimata. Infatti essi possono solo rilevare la presenza di un errore, non possono certificare l'assenza di un errore.
La verifica automatica ha un elevato costo computazionale, ma conduce un'analisi esatta. In particolare la verifica automatica può certificare l'assenza di errori, avendo esplorato tutte le possibili evoluzioni del sistema.
Si comprende dunque facilmente che l'approccio tipico sarà quello di effettuare prima testing e/o simulazionee e poi ricorrere alla verifica solo quando il sistema in esame passa la fase di testing e/o simulazione.
Testing e/o simulazione sono classici modi per cercare errori progettuali (bugs). Essi però possono solo mostrare la presenza di errori nel nostro progetto. Cioè anche se il nostro progetto passa tutti i nostri tests questo non significa che non ci sono errori. Significa solo che non abbiamo trovato alcun errore.
Per progetti non critici questo può non essere un grave problema. Se un bug appare viene fatta una release successiva. Quando però il costo dell'errore è alto in termini di vite umane (e.g. si pensi al software di controllo di un aereo) od economico (e.g. si pensi al costo sostenuto da INTEL per il noto Pentium bug) allora è opportuno usare metodi che possano garantire l'assenza di errori.
La verifica automatica è tipicamente usata su un sistema che ha già passato la fase di testing e/o simulazione. L'obiettivo della verifica automatica è dunque quello di rilevare errori che hanno una bassa probabilità di essere rilevati dal testing. Questi sono tipicamente gli errori dovuti all'uso della concorrenza.
Concettualmente la verifica automatica corrisponde all'esecuzione di tutti i possibili tests sul sistema. Naturalmente questo è in generale impossibile. I verificatori automatici raggiungono questo obiettivo usando opportuni algoritmi e strutture dati. Un metodo di verifica automatica molto efficace ed usato è il Model Checking .
Per poter introdurre la verifica automatica nel ciclo progettuale sono necessari i seguenti passi.
I requisiti del sistema da verifica possono essere definiti usando vari formalismi. Tipici esempi sono UML, MSC (Message Sequence Charts), logiche temporali (e.g. CTL, LTL, etc). Per certe proprietà (e.g. safety) è anche possibile definire i requisiti usando lo stesso linguaggio usato per definire il sistema da verificare. Un tipico esempio è l'uso delle assert nel C.
In molticasi, ma non in tutti, la proprietà da verificare può essere definita come un insieme di stati indesiderati. Quello che si vuole è che il sistema nella sua evoluzione non raggiunga mai uno stato indesiderato. In questi casi l'attività di verifica autoamtica consiste nella analisi di raggiungibilitaà, cioè nel calcolo degli insiemi di stati che il sistema può raggiungere nel corso della sua evoluzione e nel check che nessuno degli stati raggiungibili sia uno stato indesiderato.
Ecco alcuni esempi di requisiti tipici per i sistemi reattivi.
Il sistema da verificare può essere descritto usando linguaggi orientati alla definizione dell'implementazione del sistema oppure usando lingauggi orientati alla definizione dei requisiti di un sistema.
Ecco alcuni esempi di linguaggi orientati alla definizione dell'implementazione del sistema.
Ecco alcuni esempi di linguaggi orientati alla definizione dei requisiti di un sistema. Tali modelli vengono tipicamente usare per validare le specifiche informali del sistema.
Concettualmente la verifica automatica concettualmente corrisponde ad un testing esaustivo del sistema da verificare. Ovviamente eseguire un testing esaustivo non è possibile a causa delll'enorme numero di tests cases che sarebbero necessari. I model checkers ottengono lo stesso risultato utilizzando opportuni algoritmi e strutture dati. L'efficienza di tali algoritmi è di fatto il fattore che ha permesso la transizione del model checking dal mondo accademico al mondo industriale.
Ecco alcuni degli approcci usati.
La verifica automatica (model checking) può essere facilmente introdotta nel ciclo progettuale sia del software (reattivo) che dell'hardware poichè non richiede un lungo training per essere usata. Il model checking può essere usato solo su sistemi a stati finiti. Fortunatamente molti sistemi reattivi sono (o possono essere ben approssimati con) Sistemi a Stati Finiti (FSS). Per esempio rientrano in questa categoria: Hardware Digitale, Sistemi Embedded , SOC (Systems On Chip) , Protocolli , Sistemi di Controllo, Sistemi Ibridi .
In effetti in molti casi (ma non in tutti) la verifica automatica può spesso essere effettuata a partire dal codice sorgente che definisce il sistema reattivo. In questi casi fortunati non è necessaria alcuna attività di modellazione. Ad esempio esistono model checkers per: Verilog, VHDL, Esterel, SDL, Java (embedded), alcuni frammenti del C.
Per i motivi di cui sopra il model checking è ampiamente usato sia in Software Engineering che in Electrical Engineering (per il progetto di sistemi a stati finiti dal livello gate (RTL) al livello microprocessore).
Una tipica attività del Software Engineering è la formalizzazione dei requisiti del sistema da implementare e, dove necessario la sua modellazione a stati finiti in modo da poter usare un tool di verifica automatica. In alcuni casi la fase di modellazione può addirittura essere automatizzata (e.g. usando tools per abstract interpretation o control flow analysis).
Ecco alcuni esempi di tools di verifica automatica usati nel Software Engineering.
Il model checking è ormai entrato (di fatto prima chenel software) nel ciclo progettuale dell'hardware digitale. CI sono molti tools accademici ed industriali che supportano la verifica automatica nel progetto di sistemi digitali.
Bisogna inoltre tenere presente che con l'avvento dei SOC (Systems on Chip) la distinzione tra hardware e software sta diventando sempre meno netta. Usando linguaggi ad alto livello tipi VHDL o System C il progettista può definire il suo sistema rimandando ad una fase successiva la decisione di cosa verrà implmentato come hardware e cossa verrà implementato come software.
Ecco alcuni esempi di tools di verifica automatica usati nel design di hardware digitale.
Molti sistemi reattivi sono di fatto Sistemi Ibridi cioè sistemi in cui alcune variabili di stato sono continue ed altre discrete. La dinamica di tali sistemi è tipicamente descritta usando equazioni algebrico-differenziali non lineari.
Per tali sistemi l'analisi di raggiungibilità (del sistem o di un opportuno modell del sistema) è una attività complessa che può spesso essere efficientemente condotta usando un model checker.
Ecco alcuni esempi di tools di verifica automatica usati nell'analisi di sistemi ibridi.
La nostra ricerca si focalizza principalmente sui seguenti temi:
Attraverso il model checking la verifica automatica è ha avuto ormai una grande diffusione sia nel mondo accademico che in quello dell'uso nell'industria. Di fatto si è ormai nella situazione in cui molte industrie (e.g. INTEL, IBM, Microsoft, SUN, NVIDIA) contribuiscono in modo decisivo con dei propri laboratori dedicati alla verifica automatica all'avanzamento della ricerca in questo settore.
Ecco alcuni links a siti accademici ed industriali sull'argomento verifica.
A seconda del sistema da analizzare un model checker può essere più indicato doi un altro. Ecco una lista parziale di alcuni model checkers di origine accademica o industriale.