Il contributo di questa tesi consiste nell'estensione delle tecniche per la trasformazione dei programmi logici con vincoli e lo sviluppo di metodi per l'applicazione di queste tecniche alla prova di proprietà temporali di protocolli parametrizzati.ud Per prima cosa viene proposto un metodo per la prova automatica della correttezza totale delle trasformazioni che usano regole di unfolding e folding basato sulla risoluzione di sistemi di equazioni e disequazioniudsui numeri naturali.ud In secondo luogo viene proposto un metodo trasformazionale per la prova di proprietà del primo ordine di programmi logici con vincoli che manipolano liste finite di numeri razionali o reali.ud Inoltre, viene estesa la regola di trasformazione detta folding introducendo due varianti: la prima, che combina la regola di folding standard con la regola detta di clause splitting, e la seconda, che ha lo scopo di eliminare le variabili esistenziali che occorrono in una data clausola. Per la regola di folding standard e per le estensioni che vengono proposte, vengono forniti i corrispondenti algoritmi che ne permettono l'applicazione automatizzata.ud Infine, viene proposto un framework per la prova di proprietà temporali dei protocolli parametrizzati. Utilizzando questo framework viene codificato il protocollo e la proprietà che si intende provare come un programma logico. In seguito, usando la tecnica di trasformazione attraverso le regole di unfold e fold, viene verificato se la proprietà vale o meno per il dato protocollo.ud La tesi è corredata di esempi per la dimostrazione delle tecniche proposte.
展开▼
