Salvatore LA TORRE | TECNICHE AUTOMATICHE PER LA CORRETTEZZA DEL SOFTWARE
Salvatore LA TORRE TECNICHE AUTOMATICHE PER LA CORRETTEZZA DEL SOFTWARE
cod. 0522500076
TECNICHE AUTOMATICHE PER LA CORRETTEZZA DEL SOFTWARE
| 0522500076 | |
| DIPARTIMENTO DI INFORMATICA | |
| CORSO DI LAUREA MAGISTRALE | |
| INFORMATICA | |
| 2024/2025 |
| ANNO ORDINAMENTO 2016 | |
| PRIMO SEMESTRE |
| SSD | CFU | ORE | ATTIVITÀ | |
|---|---|---|---|---|
| INF/01 | 6 | 48 | LEZIONE |
| 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. |
BETA VERSION Fonte dati ESSE3 [Ultima Sincronizzazione: 2024-11-18]
