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.
