vpb

anno3/vpc/obbiettivi_del_corso

@@ -0,0 +1,7 @@
+Obiettivo del corso e' di fornire gli strumenti, teorici e pratici, necessari alla verifica dei sistemi, ed in particolare del software. Per raggiungere tale obiettivo studieremo alcuni paradigmi di base per la specifica di processi distribuiti, focalizzando l'attenzione sulle capacità modellistiche e sugli strumenti di verifica di proprietà di buon comportamento.
+
+Alla fine del corso lo studente sara' in grado di specificare sistemi concorrenti usando linguaggi formali e di utilizzare strumenti software per la verifica di proprieta' del sistema tramite verifica di proprieta' del modello. Oltre alle classiche proprieta' dei sistemi distribuiti quali assenza di deadlock, fairness e liveness, lo studente sara' in grado di definire e verificare proprieta' in logica temporale quali ad esempio: "se il processo P manda un messaggio, allora non ricevera' il prossimo messaggio sino a che non riceve un acknowledgment", oppure "se il processo P manda un messaggio, ricevera' un acknowledge entro 5 unita' di tempo".
+
+Il corso non ha come obiettivo di fornire conoscenza su strumenti di verifica di linguaggi di programmazione, perche'  non si focalizza sulla verifica dell' implementazione degli algoritmi, ma sulla verifica delle soluzioni algoritmiche legate alla concorrenza.
+Nel ciclo di sviluppo del software le competenze acquisite in questo corso sono utili al fine della progettazione e verifica di soluzioni concorrenti/distribuite
+Ultime modifiche: lunedì, 22 febbraio 2016, 11:06

anno3/vpc/testi

@@ -0,0 +1,13 @@
+Testo su reactive systems (CCS, Equivalenze e Timed Automata)
+
+Il testo "Reactive Systems: Modelling, specification and verification" di Luca Aceto e colleghi e'  un ottimo libro di testo, soprattutto per quanto riguarda la parte su CCS, equivalenze e timed system.
+
+Il pdf dei primi capitoli del libro si trova facilmente in rete, su siti legali (universita'  di appartenenza degli autori http://www.cs.ioc.ee/yik/schools/win2007/ingolfsdottir/sv-book-part1.pdf e ), mentre la versione integrale  stampata e'  disponibile presso la biblioteca del Diaprtimento di Informatica.
+
+Ultime modifiche: lunedì, 2 marzo 2020, 14:08
+
+
+ALTRO:
+
+seven_myths_of_formal_methods
+Teaching Formal Methods for Software Engineering –Ten Principles

anno3/vpc/verifica_apprendimento

@@ -0,0 +1,16 @@
+Combinazione di:
+
+Piccoli esercizi e più consistenti progetti durante il corso, con precise date di consegna (pencil and paper and use of tools)
+
+Gli esercizi devono essere accompagnati da una relazione (written report)
+
+Verifica finale – discussione degli esercizi con uso dei tool e verifica della parte di teoria  (dates can be agreed upon with the teacher, contact the teacher at least 10 days before)
+
+Ci sono due modalita’ per la valutazione
+
+Orientata agli strumenti:  sperimentazioni complete con gli strumenti di verifica. Discussione dei laboratori e una prova orale sugli argomenti principali
+
+Orientata alla teoria: esercizi piu’ semplici e classico esame di teoria su tutti gli argomenti del corso
+
+
+Ultime modifiche: lunedì, 22 febbraio 2016, 11:07