RICERCA ITALIANA     

Integrazione di metodi di ragionamento automatico nel model checking: verifica formale automatica di sistemi di grande scala e a stati infiniti.

Università degli Studi di Genova

Abstract

I sistemi informatici sono sempre più presenti nella nostra vita
quotidiana. Ad esempio ci si affida a sistemi elettronici
programmabili complessi per la supervisione di funzionalità critiche
di automobili, aerei e siti industriali, dove l'affidabilità dei
componenti hardware e software è di importanza capitale. Tuttavia le
tecniche di verifica tradizionali come la simulazione ed il testing
non garantiscono l'assenza di errori e questo ha un forte impatto
sull'affidabilità dei componenti prodotti. I metodi formali invece,
introducendo rigore formale nelle fasi di specifica, design e
verifica, permettono di ottenere il livello di affidabilità
necessario. Tuttavia applicare manualmente le tecniche di verifica
formale a software e hardware di scala industriale è impraticabile,
anche solo per la loro dimensione. Ecco perché è cruciale lo sviluppo
di tecniche automatiche di verifica formale.

Tra esse il Model Checking (MC) è emerso come tecnica automatica di
maggior successo per la verifica formale di sistemi a stati finiti
come p.e. i circuiti hardware e i protocolli di comunicazione. Il MC è
stato usato con successo per verificare svariati design di hardware
industriale come il protocollo di cache coherence IEEE Futurebus+. Si
noti che il successo del MC è dovuto in larga parte a sviluppi nel
ragionamento automatico >>>

Coordinatore Scientifico del Programma di Ricerca

Alessandro Armando Università degli Studi di GENOVA

Obiettivo del Programma di Ricerca

La crescita in dimensione e complessità dei sistemi hardware e
software rinnova la sfida di realizzare strumenti automatici di
qualità per la loro validazione. Alle tecniche basate sul testing si
devono affiancare strumenti complementari, in quanto il testing
esaustivo non è praticabile su sistemi di complessità industriale, e
test parziali possono fallire nel rilevare errori. Inoltre, il testing
sistematico è costoso. Negli ultimi vent'anni, il model checking è
emerso come la principale tecnica in grado di complementare il
testing. La difficoltà intrinseca dei problemi (enorme numero di stati
per i sistemi hardware, numero infinito di stati per i sistemi
software) ha portato all'evoluzione delle tecniche di model checking
da metodi che enumerano esplicitamente gli stati a tecniche basate su
rappresentazioni simboliche degli stati e metodi basati
sull'astrazione. Il presente progetto riguarda lo sviluppo di tecniche
di ragionamento automatico per il supporto di procedure avanzate di
model checking.

Il ragionamento automatico sta assumendo un ruolo crescente in quanto
l'analisi dei sistemi hardware e software richiede l'utilizzo di
logiche sempre più espressive. Ad esempio, per fronteggiare l'aumento
di complessità dei circuiti hardware si adottano modelli di più alto
livello rispetto a quello delle >>>

Risultati parziali attesi

L'obiettivo finale del progetto è lo sviluppo di una nuova generazione
di tool per il model-checking capace di verificare automaticamente
software, RTL hardware design e, più in generale, sistemi di grandi
dimensioni o a stati infiniti. Questo obiettivo ambizioso sarà
perseguito basandosi sulle migliori tecniche di ragionamento
automatico ed attraverso la loro effettiva integrazione con le
procedure di model checking allo stato dell'arte. In caso di successo,
il progetto avrà un impatto significativo sia nella comunità di
ricerca che si occupa di Ragionamento Automatico, che in quella che si
occupa di Metodi Formali. Le tecniche di verifica sviluppate
nell'ambito del progetto incrementeranno sia la produttività che la
sicurezza di sistemi software e hardware critici.

La ricerca di procedure di decisione espressive efficienti e
scalabili, cosiccome le teorie decidibili e la loro applicazione a
compiti di verifica, è uno degli argomenti più importanti nel campo
dell'Informatica. In caso di successo, il progetto porterà ad una
svolta nell'applicazione di tecniche di ragionamento automatico alla
verifica formale, raccogliendo i benefici degli investimenti fatti
nello sviluppo dei migliori theorem prover automatici (solutori SAT,
solutori SMT e theorem prover per logiche clausali con uguaglianze).

I >>>

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

- Model Checking per Verifica di Software e Hardware Design

L'astrazione ed il raffinamento guidati da controesempio (CEGAR) [12]
è la tecnica di maggior successo che permette l'applicazione del MC al
software. Dato un programma P, essa consiste nella costruzione di
un'astrazione finita P' che preserva le proprietà di P e
nell'applicare poi tecniche di Software MC (SMC) a P'. Se P' è
corretto, lo è anche P, altrimenti l'algoritmo di SMC dà una traccia
(astratta) di errore. La traccia può essere spuria, dato che P'
modella un sovrainsieme dei comportamenti di P per definizione di
astrazione. La traccia viene sottoposta ad un controllo di
compatibilità in P. Se risulta compatibile, è una traccia "reale" e
CEGAR si ferma riportando l'errore all'utente. Altrimenti, dalla
traccia vengono estratti (con l'aiuto di un theorem prover) dati utili
a costruire una nuova astrazione di P che non contenga il
comportamento errato riscontrato. A testimoniare il successo e
l'applicabilità di tale tecnica vi sono un vasto numero di lavori
scientifici tra cui [12-16,62] e l'interesse da parte di industrie
leader quali p.e. Microsoft [2].

Il SMC è stato applicato con successo anche a sistemi a stati finiti
di grande dimensione (p.e. in [17]) per lenire il noto problema >>>