Appunti degli studenti per corsi ed esami del Prof. Gerla Brunella

Appunti e Documenti pubblicati dagli studenti che hanno frequentato i suoi corsi. I materiali caricati riguardano gli insegnamenti di logica matematica, algebra e geometria nel settore disciplinare di Scienze matematiche e informatiche sostenuti presso l’università di Università degli Studi dell' Insubria.

…continua

Cerca appunti per esame

Università

Università degli Studi dell' Insubria

Esami di riferimento

Algebra e geometria| Logica matematica

I materiali pubblicati sul sito costituiscono rielaborazioni personali del Publisher di informazioni apprese con la frequenza delle lezioni e lo studio autonomo di eventuali testi di riferimento in preparazione all’esame finale o della tesi. Non devono intendersi come materiale ufficiale dell’università attribuibile al docente del corso.

…continua

Appunti degli studenti per corsi ed esami del Prof. Gerla Brunella

Model checking per l’analisi di un algoritmo di autenticazione a chiave pubblica

Esame Logica matematica

Facoltà Scienze matematiche fisiche e naturali

Dal corso del Prof. B. Gerla

Università Università degli Studi dell' Insubria

Tesi

Scarica

La nostra società dipende sempre più da sistemi informatici e software in quasi ogni aspetto della vita quotidiana. Spesso non ci rendiamo nemmeno conto che sono coinvolti computer e software. Quindi, la sfida principale per il campo dell’informatica è quella di fornire formalismi, tecniche e strumenti che consentano la progettazione efficiente di sistemi corretti e ben funzionanti, nonostante la loro complessità. Per evitare errori e malfunzionamenti di questi dispositivi, ci sono delle tecniche di verifica importanti quali la simulazione, il testing, la verifica formale e infine il Model Checking, su cui è incentrato questo lavoro di tesi. Il Model Checking è un algoritmo di verifica formale introdotto agli inizi degli anni ’80 da Clarke & Emerson (USA) e contemporaneamente da Quielle & Sifakis (Francia). È una tecnica automatica per verificare le proprietà di correttezza dei sistemi reattivi critici per la sicurezza. uesto metodo è stato applicato con successo per trovare errori sottili in progetti industriali complessi come circuiti sequenziali, protocolli di comunicazione e controllori digitali. Ci sono stati moltissimi errori di software e hardware che sono ancora oggi noti esempi drammatici. Possiamo ricordare tra i più importanti: il bug dell'unità di divisione in virgola mobile del Pentium di Intel all'inizio degli anni Novanta, il caso Therac-25, il caso del sistema bagagli automatico dell’aeroporto di Denver, il caso della compagnia telefonica AT&T e l’autodistruzione del razzo Ariane 5.La tecnica del Model Checking è uno dei più significativi avanzamenti della ricerca in Informatica di base di questi ultimi decenni: nella verifica tramite Model Checking il sistema sotto analisi viene descritto con un linguaggio formale e successivamente modellato mediante automi a stati. Questa tecnica è totalmente automatica ed ogni volta che viene violata una proprietà desiderata, viene fornito un controesempio che illustra un comportamento che falsifica tale proprietà.

...continua