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 | |
| 2019/2020 |
| ANNO CORSO 2 | |
| 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. MODEL-CHECKING LA TECNOLOGIA DEL MODEL-CHECKING CONCETTI BASE FONDAMENTI: AUTOMI, LOGICA TEMPORALE, COMPLESSITÀ COMPUTAZIONALE MODEL-CHECKING ESPLICITO MODEL-CHECKING SIMBOLICO BOUNDED MODEL-CHECKING MODEL-CHECKING CON AUTOMI PUSHDOWN MODEL-CHECKING DI CODICE SORGENTE ASTRAZIONE RAFFINAMENTO DELLE ASTRAZIONI GUIDATE DAL CONTROESEMPIO (CEGAR LOOP) IMPLEMENTAZIONE DI MODEL-CHECKERS CON FIXED-POINT LOGIC PROGRAMMI CONCORRENTI BOUNDED-CONTEXT SWITCHING SEQUENZIALIZZAZIONE MODEL-BASED TESTING CON MODEL-CHECKERS |
| 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 AL RESTO DELLA CLASSE E DISCUSSIONE CRITICA SUI CONCETTI E METODI ESPOSTI. COLLOQUIO ORALE SUGLI ARGOMENTI SVOLTI AL CORSO. 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 |
BETA VERSION Fonte dati ESSE3 [Ultima Sincronizzazione: 2021-02-19]
