Formal Methods in System Analysis

ΑΠΟΤΕΛΕΣΜΑΤΑ ΕΞΕΤΑΣΕΩΝ ΙΟΥΝΙΟΥ 2007

Slides

• Course Presentation (Παρουσίαση Μαθήματος) - pdf version
• Introduction - Propositional Calculus (Εισαγωγή - Προτασιακός Λογισμός) - pdf version
• Predicate Calculus (Κατηγορηματικός Λογισμός) - pdf version
• Program Verification (Επαλήθευση Προγραμμάτων) - pdf version
• Model Checking Automata (Έλεγχος Μοντέλων με Αυτόματα) - pdf version
• Computation Tree Temporal Logic (Χρονική Λογική) - pdf version
• Reachability, Safety, Liveness and Fairness (Προσεγγισιμότητα, Ασφάλεια, Βιωσιμότητα & Αμεροληψία) - pdf version
• Exercises in Temporal Logic (Ασκήσεις στη Χρονική Λογική) - pdf version - SOLUTIONS

Recommended Books

• Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, Ph. and McKenzie, P., Systems and Software Verification: Model-checking techniques and tools, Springer, 2001 (ACM link)  

Coursework & Presentations (6/7/2007)

• Coursework 2007 (Εκφωνήσεις εργασιών 2007)
• The ABP protocol (by E. Moka and A. Belogia) - Coloured Petri Net Model
• The Dekker Mutual Exclusion Algorithm (by L. Nanos and V. Tzialamani) - Coloured Petri Net Model
• The Franklin & Reiter e-Commerce Protocol (by L. Zagkaretos and V. Karageorgou) - Coloured Petri Net Model
• The Java Modeling Language (by H. Kargioti) - Report - Demo Applications

Interesting Readings

• Holzmann, G. J., Design and validation of computer protocols, Prentice-Hall, 1991
• Gluch, D. P., Weistock, C. B., Model-Based Verification: A Technology for Dependable System Upgrade, Carnegie Mellon, 1998

Formal Analysis Tools

• Introduction to the SPIN Model Checker (presentation by S. Basagiannis) - Installation instructions
• The SPIN model checker official website
• The CPN TOOLS (Coloured Petri Net Tools) official website
• CPN Tools (presentation by Kurt Jensen)
• CPN ML Basics (presentation)
• Probabilistic Model Checking with PRISM (presentation by Nikos Alexiou)