2. Docenti
  3. LA TORRE Salvatore
  4. Didattica

TECNICHE AUTOMATICHE PER LA CORRETTEZZA DEL SOFTWARE

Salvatore LA TORRE TECNICHE AUTOMATICHE PER LA CORRETTEZZA DEL SOFTWARE

0522500076
DIPARTIMENTO DI INFORMATICA
CORSO DI LAUREA MAGISTRALE
INFORMATICA
2024/2025



ANNO ORDINAMENTO 2016
PRIMO SEMESTRE
CFUOREATTIVITÀ
648LEZIONE
SALVATORE LA TORRE T Curriculum
AppelloData
APPELLO PROF. LA TORRE 08/01/2025 - 12:00
APPELLO PROF. LA TORRE 08/01/2025 - 12:00
Obiettivi
CONOSCENZA E CAPACITÀ DI COMPRENSIONE
ACQUISIZIONE DELLE COMPETENZE DI BASE SULLE TECNICHE DI VERIFICA AUTOMATICA BASATE SU MODEL-CHECKING E TESTING. COMPRENDERE LE DIFFERENZE E LA COMPLEMENTARIETÀ TRA QUESTE METODOLOGIE E ALTRE METODOLOGIE DI VERIFICA UTILIZZATE IN PRATICA.
ACQUISIRE FAMILIARITÀ CON LE PROBLEMATICHE LEGATE ALL'UTILIZZO DI QUESTE TECNOLOGIE E LE PRINCIPALI SOLUZIONI ADOTTATE. COMPRENDERE GLI ALGORITMI SVILUPPATI.

CAPACITÀ DI APPLICARE CONOSCENZA E COMPRENSIONE
CAPACITÀ DI INDIVIDUARE LA CLASSE DI MODELLI E I LINGUAGGI DI SPECIFICA PIÙ APPROPRIATI RISPETTO AI PROGRAMMI DA ANALIZZARE. CAPACITÀ DI UTILIZZARE UN MODEL-CHECKER PER ESEGUIRE LE VERIFICHE DI CORRETTEZZA SU SISTEMI REALI. CAPACITÀ DI MODULARE LE RISORSE DI COMPUTAZIONE PER POTER UTILIZZARE IL MODEL-CHECKING PER PROGRAMMI MOLTO COMPLESSI.
Prerequisiti
CONOSCENZE DI BASE SU AUTOMI FINITI, AUTOMI PUSHDOWN, PROGRAMMAZIONE PROCEDURALE, LOGICA BOOLEANA E COMPLESSITÀ COMPUTAZIONALE.
Contenuti
INTRODUZIONE, CORRETTEZZA DEI PROGRAMMI, SPECIFICHE E CONCETTO DI ERRORE, STRUMENTI PER VERIFICARE LA CORRETTEZZA DEL SOFTWARE, CENNI SUL TESTING (4 ORE)

LA TECNOLOGIA DEL MODEL-CHECKING, CONCETTI DI BASE (2 ORE)

FONDAMENTI: AUTOMI, LOGICA TEMPORALE, COMPLESSITÀ COMPUTAZIONALE (8 ORE)

MODEL-CHECKING ESPLICITO (4 ORE)
MODEL-CHECKING SIMBOLICO (4 ORE)
BOUNDED MODEL-CHECKING (4 ORE)
MODEL-CHECKING CON AUTOMI PUSHDOWN (4 ORE)

MODEL-CHECKING DI CODICE SORGENTE, ASTRAZIONE
RAFFINAMENTO DELLE ASTRAZIONI GUIDATE DAL CONTROESEMPIO: CEGAR LOOP (4 ORE)

IMPLEMENTAZIONE DI MODEL-CHECKERS CON FIXED-POINT LOGIC (4 ORE)

PROGRAMMI CONCORRENTI, BOUNDED-CONTEXT SWITCHING, SEQUENZIALIZZAZIONE (8 ORE)

MODEL-BASED TESTING CON MODEL-CHECKERS (2 ORE)
Metodi Didattici
LA PARTE TEORICA DEL CORSO VIENE SVILUPPATA CON LEZIONI FRONTALI IN AULA. GLI ARGOMENTI IN PROGRAMMA VENGONO PRESENTATI CON L'AUSILIO DI PRESENTAZIONI POWERPOINT O ANALOGO. SU OGNI CONCETTO VIENE AVVIATA UNA DISCUSSIONE CRITICA CON LA CLASSE E OVE APPROPRIATO SI EFFETTUANO CONFRONTI CON SOLUZIONI ALTERNATIVE.
LA PARTE PRATICA VIENE SVOLTA CON SPERIMENTAZIONE DIRETTA SUL PC. IN PARTICOLARE, SI IMPLEMENTANO MODELLI DI PROGRAMMI, OPPURE
SI PRENDONO PROGRAMMI O MODELLI DAI BENCHMARK DISPONIBILI PER I VARI TOOLS, E SI ESEGUONO SESSIONI DI VERIFICA E ANALISI DEI RISULTATI OTTENUTI. LA SPERIMENTAZIONE AVVIENE IN MANIERA INDIVIDUALE ED È SEGUITA DA UNA DISCUSSIONE IN CUI SI CONFRONTANO LE ESPERIENZE FATTE.
Verifica dell'apprendimento
PROGETTO INDIVIDUALE DI APPROFONDIMENTO SU TEMATICHE ATTINENTI IL PROGRAMMA DEL CORSO.
PRESENTAZIONE DEL PROGETTO E DISCUSSIONE CRITICA SUI CONCETTI E METODI ESPOSTI.
COLLOQUIO ORALE SUGLI ARGOMENTI SVOLTI AL CORSO.
L'ABILITÀ DI SVILUPPARE IL PROGETTO IN AUTONOMIA, L'ABILITÀ DI INDIVIDUARE GLI ASPETTI PRINCIPALI DEGLI ARGOMENTI PROPOSTI, LA CONOSCENZA APPROFONDITA DEI DETTAGLI TECNICI E DELLE CONSEGUENZE PRATICHE, E LA CHIAREZZA DELLA PRESENTAZIONE SARANNO VALUTATE POSITIVAMENTE.
LA VALUTAZIONE VERRÀ ESPRESSA IN TRENTESIMI E TERRÀ CONTO DI TUTTI GLI ASPETTI SOPRAELENCATI.
Testi
•MORDECHAI BEN-ARI
PRICIPLES OF THE SPIN MODEL CHECKER
SPRINGER, ISBN 978-1-84628-769-5
•GERARD J. HOLZMANN
THE SPIN MODEL CHECKER: PRIMER AND REFERENCE MANUAL
ADDISON WESLEY, ISBN 0-321-22862-6
•NOTE DELLE LEZIONI E ARTICOLI SCIENTIFICI CITATI
Altre Informazioni
LA FREQUENZA ALLE LEZIONI È FORTEMENTE CONSIGLIATA.
Orari Lezioni

  BETA VERSION Fonte dati ESSE3 [Ultima Sincronizzazione: 2024-12-13]