Salvatore LA TORRE | VERIFICA DI PROGRAMMI I
Salvatore LA TORRE VERIFICA DI PROGRAMMI I
cod. 0522500049
VERIFICA DI PROGRAMMI I
| 0522500049 | |
| DIPARTIMENTO DI INFORMATICA | |
| CORSO DI LAUREA MAGISTRALE | |
| INFORMATICA | |
| 2014/2015 |
| ANNO CORSO 2 | |
| ANNO ORDINAMENTO 2010 | |
| PRIMO SEMESTRE |
| SSD | CFU | ORE | ATTIVITÀ | |
|---|---|---|---|---|
| INF/01 | 4 | 32 | LEZIONE | |
| INF/01 | 2 | 24 | LABORATORIO |
| Obiettivi | |
|---|---|
| -CONOSCENZA E CAPACITÀ DI COMPRENSIONE: ACQUISIZIONE DELLE COMPETENZE DI BASE SULLE TECNICHE DI VERIFICA AUTOMATICA DI TIPO MODEL-CHECKING. COMPRENDERE LE DIFFERENZE E LA COMPLEMENTARIETÀ TRA QUESTA METODOLOGIA E ALTRE METODOLOGIE DI VERIFICA UTILIZZATE IN PRATICA. ACQUISIRE FAMILIARITÀ CON LE PROBLEMATICHE LEGATE ALL'UTILIZZO DI QUESTA TECNOLOGIA E LE PRINCIPALI SOLUZIONI ADOTTATE. COMPRENDERE GLI ALGORITMI DI DECISIONE UTILIZZATI PER DIVERSE CLASSI DI SISTEMI E LINGUAGGI DI SPECIFICA. -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. -AUTONOMIA DI GIUDIZIO: DISCUSSIONE DEI PRO E I CONTRO DELLE TECNICHE E SOLUZIONI STUDIATE. ANALISI CRITICA DEI LAVORI PROGETTUALI. RICERCA INDIVIDUALE DELLE FONTI SCIENTIFICHE PER APPROFONDIMENTI SU ARGOMENTI A SCELTA. -ABILITÀ COMUNICATIVE: PARTECIPAZIONE ALLA FORMULAZIONE DELLE STRATEGIE RISOLUTIVE RISPETTO AI PROBLEMI PROPOSTI. PRESENTAZIONE E DISCUSSIONE DELLE SOLUZIONI INDIVIDUATE. PARTECIPAZIONE ATTIVA ALLE LEZIONI AI SEMINARI DI APPROFONDIMENTO. -CAPACITÀ DI APPRENDERE: STUDIO INDIVIDUALE DI MATERIALE DI APPROFONDIMENTO. RICERCA DI NUOVI TOOL PER CLASSI DI PROGRAMMI DI INTERESSE. |
| Prerequisiti | |
|---|---|
| CONOSCENZE DI BASE SU AUTOMI FINITI, AUTOMI PUSHDOWN, PROGRAMMAZIONE PROCEDURALE, LOGICA BOOLEANA E COMPLESSITÀ COMPUTAZIONALE. |
| Contenuti | |
|---|---|
| IL PROGRAMMA È DIVISO IN DUE PARTI: PROGRAMMI A STATI FINITI E PROGRAMMI CON CHIAMATE RICORSIVE. PARTE I - PROGRAMMI A STATI FINITI CORRETTEZZA DEI PROGRAMMI. DIFFICOLTÀ E NECESSITÀ DI UTILIZZARE STRUMENTI AUTOMATICI. LA TECNOLOGIA DEL MODEL-CHECKING. CONCETTI BASE. IL MODEL-CHECKER SPIN. MODELLAZIONE DI SISTEMI IN SPIN: LINGUAGGIO PROMELA. SCRITTURA DI PROGRAMMI SEQUENZIALI IN PROMELA. CONCETTO DI ASSERZIONE. VERIFICA DI PROGRAMMI SEQUENZIALI IN SPIN. CONCETTI BASE DELLA COMPUTAZIONE CONCORRENTE: INTERLEAVING, ATOMICITÀ, INTERFERENZA. VERIFICA DI SISTEMI CONCORRENTI CON ASSERZIONI: IL PROBLEMA DELLA CRITICAL SECTION. SINCRONIZZAZIONE: COSTRUTTO ATOMIC, SEMAFORI. TERMINAZIONE DI PROCESSI. SPECIFICHE DI PROPRIETÀ DI CORRETTEZZA PIÙ GENERALI: LOGICA TEMPORALE. SAFETY, LIVENESS E FAIRNESS. MODELLAZIONE DI UNA NON-CRITICAL SECTION. STRUTTURE DATI E DI CONTROLLO IN PROMELA. CANALI IN PROMELA. MODELLAZIONE DI AUTOMI FINITI IN PROMELA. VERIFICA DI AUTOMI FINITI. USO DI SPIN COME SAT SOLVER. SPECIFICATORI PER VARIABILI. VARIABILI PREDEFINITE. PRIORITÀ. MODELLAZIONE DI ECCEZIONI. LEGGERE DALLO STANDARD INPUT. CASI DI STUDIO: MODELLAZIONE DI ALGORITMI DI SCHEDULING REAL-TIME. ALGORITMO DI FISCHER. MODELLAZIONE DI SISTEMI DISTRIBUITI. MODELLAZIONE E VERIFICA DI UN SISTEMA DI COMUNICAZIONI TELEFONICHE. APPROFONDIMENTI SU SPIN: VISITA DEGLI STATI, OTTIMIZZAZIONI. VERIFICA DI PROGRAMMI C. CODICE C EMBEDDED. ESTRAZIONE DI MODELLI DA PROGRAMMI C. USO DI MODEX E LOOKUP TABLE. CONCETTO DI ASTRAZIONE. SOUNDNESS E COMPLETENESS DI ASTRAZIONI. MODELLI DI ASTRAZIONE: SELECTIVE DATA HIDING, SELECTIVE RESTRICTION, DATA TYPE ABSTRACTION.
|
| 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 TOOL, 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. SONO VALUTATI POSITIVAMENTE L'INDIPENDENZA NELLO STUDIO, LA CAPACITÀ DI SELEZIONARE GLI ASPETTI PRINCIPALI DELLE TEMATICHE PROPOSTE, LA COMPRENSIONE DEI DETTAGLI TECNICI E DELLE CONSEGUENZE PRATICHE, E LA CHIAREZZA ESPOSITIVA. |
| 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 | |
|---|---|
| HTTP://WWW.DI.UNISA.IT/PROFESSORI/LATORRE/DIDATTICA/VP1/ |
BETA VERSION Fonte dati ESSE3 [Ultima Sincronizzazione: 2016-09-30]
