Metodi di ragionamento automatico per l'analisi di hardware e software: progetto, integrazione, applicazione - Grandi macchine di prova come piccole macchine di prova: progetto, integrazione ed applicazione all'analisi di programmi (PRIN 2006 valutato positivamente ma non finanziato)

Data inizio
9 febbraio 2007
Durata (mesi) 
24
Dipartimenti
Informatica
Responsabili (o referenti locali)
Bonacina Maria Paola
Parole chiave
RAGIONAMENTO AUTOMATICO, ANALISI DI SOFTWARE ED HARDWARE, DEDUZIONE AUTOMATICA

Metodi di ragionamento automatico per l'analisi di hardware e software: progetto, integrazione, applicazione

Secondo uno studio dello U.S. National Institute for Standards and Technologies (NIST Planning Report 02-3, The Economic Impacts of Inadequate Infrastructure for Software Testing, June 2002, http://www.nist.gov/director/prog-ofc/report02-3.pdf) si stima che gli errori nei programmi costino all'economia statunitense $59.9 miliardi l'anno, di cui il 60% e` sopportato dagli utenti ed il resto da sviluppatori e venditori. Quello studio trovo` che sotto ragionevoli assunzioni si potrebbe evitare piu` di un terzo di quei costi mediante tecniche che permettano una piu` precoce ed efficace identificazione e rimozione di difetti software. E` verosimile che costi e potenziali risparmi siano dello stesso ordine di grandezza nella U.E. Gli errori software minano la sicurezza e l'accessibilita` degli elaboratori. I pirati effettuano intrusioni negli elaboratori attaccando le vulnerabilita` dei servizi offerti da qualsiasi elaboratore in rete. Virus o "vermi" su Internet sfruttano il sovraccarico di buffer in server di posta o di rete. Poiche` cosi` tante attivita` ne dipendono, qualsiasi miglioramento nella curva costo/qualita` del software avrebbe un ampio impatto sociale ed economico.

Gli attuali sistemi software presentano nuove sfide, perche` comportano infiniti stati, applicazioni distribuite e proprieta` non funzionali. Gli approcci alla qualita` sono orientati o al processo o all'evidenza, dove la principale tecnica orientata all'evidenza e` il testing. Il testing e` costoso e non puo` essere esaustivo. Complementari al testing sono le tecniche analitiche, dove il primato storico spetta all'analisi statica. Il piu` delle tecniche analitiche e` semi-automatico e richiede la preparazione degli utenti. Se tutte queste metodologie sono complementari, l'importanza del problema rende necessario investigare tecniche automatiche, che portino a strumenti push-button.

I successi del model checking nella verifica di hardware suggerirono di studiare il model checking di software. Questo pero` e` molto piu` arduo, perche` richiede modelli con numero infinito di stati. Inoltre, l'analisi di hardware e` lungi dall'essere un problema risolto. La crescente complessita` dei sistemi hardware ed il trasferimento di funzionalita` da software a hardware sfumano i confini tra le analisi dell'uno e dell'altro ed i loro requisiti.

Una ragione dei successi del model checking di hardware e` la possibilita` di ridurre il problema a istanze di SAT ed applicare solutori SAT efficienti. La maggior causa di difficolta` con il model checking di software e forme piu` avanzate di model checking di hardware e` che il ragionamento proposizionale non basta. Occorre il ragionamento automatico in aritmetica, logica equazionale, frammenti di logica del prim'ordine.

L'obbiettivo del progetto e` migliorare il ragionamento automatico per l'analisi di software ed hardware, definendo, progettando ed implementando procedure di decisione per l'uguaglianza, l'aritmetica lineare, le strutture di dati e loro combinazioni. Tali procedure devono essere:

* facili da costruire
* facili da combinare
* tali da produrre la prova
* efficienti
* capaci di scalare
* incrementali

ed integrate in strumenti di verifica.

Poiche` nessuna tecnica da sola soddisfa tutti i requisiti, il progetto trarra` il massimo dalle tecnologie esistenti per SAT, dimostrazione automatica e model checking, per costruire procedure di decisione ed incorporarle in nuovi verificatori.

I proponenti offrono la giusta combinazione di competenze:

* Dimostrazione automatica, procedure di decisione equazionali (UNIVR)
* SAT, procedure di decisione equazionali e basate su SAT, model checking di software (UNIGE)
* Model checking di software (UNINA)
* Procedure di decisione basate su SAT, model checking (UNITN)

Questo progetto avvicinera` una nuova generazione di strumenti di model checking, che combinino la velocita` dei solutori SAT con l'espressivita` necessaria per l'analisi di software ed hardware.

Enti finanziatori:

PRIN VALUTATO POSITIVAMENTE
Finanziamento: richiesto
Programma: COFIN - Progetti di Ricerca di Interesse Nazionale

Partecipanti al progetto

Maria Paola Bonacina
Professore ordinario
Aree di ricerca coinvolte dal progetto
Sistemi intelligenti
Computing methodologies - Artificial intelligence

Attività

Strutture