A syntactic-semantic approach for incremental program verification of matching logic properties

Il processo di sviluppo software non e monolitico, ma si compone di una sequenza di passaggi intermedi. In pratica, il software e continuamente sottoposto a modifiche; sia relativamente a specifiche e requisiti, a causa di cambiamenti nell'ambiente circostante o nei bisogni dell'utente; sia nell'implementazione, per la correzione di errori esistenti o per l'aggiunta di nuove funzionalita. In entrambi i casi, il cambiamento e una caratteristica peculiare del software, presente in quasi ogni fase del ciclo di sviluppo. D'altro canto, le tecniche di verifica formale diventano man mano piu efficaci nell'aiutare lo sviluppatore software. Tuttavia a questo miglioramento tecnologico non corrisponde un eguale diffusione dell'uso di tali tecniche nel controllo della correttezza del software. Un motivo di cio e da ricercare nell'elevata richiesta di risorse computazionali delle tecniche di verifica formali, dovute alle complessita computazionali presenti. Riteniamo che la natura essenzialmente incrementale del software possa essere sfruttata per sviluppare tecniche di verifica piu efficienti. Molti approcci di verifica formale esistenti, infatti, non sfruttano il fatto di essere applicati ad una sequenza di versioni del software, che differiscono poco tra loro; verificando da zero ogni nuova versione. Una soluzione efficiente e data da tecniche di verifica formale incrementali: approcci che sono capaci di riutilizzare i risultati delle computazioni intermedie ottenute durante la verifica di una versione precedente del software, per velocizzare la verifica delle versioni successive. L'obiettivo e di rendere la verifica formale un modo usabile e pratico per garantire la qualita dei prodotti software. Ad oggi, la tecnica di verifica piu utilizzata e il testing, che si e largamente diffusa con l'avvento delle tecniche di sviluppo Agile. L'applicazione a sistemi software in continua evoluzione ha prodotto il testing continuo: ad ogni nuova versione del prodotto sofware vengono applicate automaticamente un insieme di casi di test. Il fine ultimo e quindi quello di ottenere un approccio di verifica formale incrementale, che possa complementare il testing, risultando allo stesso modo conveniente e pratico da usare, fornendo pero, nel contempo, solide garanzie sulla correttezza del software verificato. Le tecniche analizzate si basano sulla struttura sintattica del prodotto software verificato. Il linguaggio formale utilizzato per definire il sofware viene sfruttato per identificare i cambiamenti ad un livello sintattico: il software viene descritto da grammatiche a precedenza di operatori, che grazie e proprieta quali la localita, permettono di effettuare il parsing solo delle parti toccate dal cambiamento. L'incrementalita ottenuta a livello sintattico viene poi riportata a livello semantico attraverso l'uso di grammatiche ad attributi: utilizzando grammatiche composte da soli attributi sintetizzati, l'effetto semantico delle modifiche apportate e ristretto a una parte dell'albero sintattico. Quest'intuizione e stata sviluppata nel framework SiDECAR, che consente di definire una tecnica di verifica incrementale su un dato linguaggio di programmazione. In questo lavoro, tale tecnica generale viene applicata al caso della verifica di proprieta specificate in matching logic. La matching logic e un sistema di verifica alla Hoare fondato sulla semantica formale del linguaggio. In particolare abbiamo analizzato il caso del linguaggio KernelC, un sottoinsieme del C che mantiene caratteristiche interessanti quali la gestione della memoria, i cicli, le chiamate a funzione e la ricorsione. Abbiamo sviluppato un framework per la verifica della matching logic condotta attraverso la valutazione di attributi semantici. Su questo approccio abbiamo sviluppato la nostra tecnica di verifica incrementale. Abbiamo poi implementato questo approccio all'interno del framework SiDECAR, consentendo la verifica incrementale di programmi KernelC specificati tramite matching logic. Abbiamo condotto una valutazione sperimentale sul nostro approccio di verifica incrementale utilizzato un grande insieme di programmi, contenenti diverse versioni ciascuno; abbiamo poi confrontato il nostro approccio col tool MATCHC, che definisce lo stato dell'arte nella verifica matching logic non incrementale di programmi KernelC. Piu precisamente, abbiamo prima confrontato il nostro tool con MATCHC sugli esempi forniti da MATCHC. Abbiamo poi valutato l'approccio incrementale su programmi o ottenuti tramite mutazioni casuali sugli esempi MATCHC, o tratti da benchmark noti, come la suite di test Siemens, o da strutture classiche note in letteratura, come gli alberi rosso-neri. I risultati ottenuti mostrano che il nostro approccio incrementale e effettivamente piu efficiente, nella verifica di proprieta matching logic su programmi KernelC, rispetto alla verifica non-incrementale.