ΕΠΛ 664: Ανάλυση και Επαλήθευση Συστημάτων
Class Notes


Η ιστοσελίδα αυτή θα ενημερώνεται τακτικά με τις διαφάνειες των διαλέξεων σε μορφή pdf.
 
 
Διάλεξη 0
ΕΠΛ664
 - Περιγραφή και στόχοι του μαθήματος
download (pdf)
Διάλεξη 1
Εισαγωγή
 - Εισαγωγική Περιγραφή του Μαθήματος
download (pdf)
Διαλέξεις 2-3
Αρχές Μοντελοποίησης Συστημάτων
 - Μοντελοποιήση σειριακών και συντρέχοντων συστημάτων, συστήματα μεταβάσεων, δικαιοσύνη αναπαράσταση ταυτοχρονισμού με παρεμβαλλόμενη και μερική διάταξη
download (pdf)
Διαλέξεις 4-5
Γραμμική Χρονική Λογική 
 - Γραμμική Χρονική Λογική (σύνταξη και ερμηνεία), Διατύπωση ιδιοτήτων, Δομές Kripke, Μοντελοέλεγχος
download (pdf)
Διάλεξη 6
Aυτοματοποιημένη Επαλήθευση 
 - Έλεγχος μοντέλου με αλγόριθμους γράφων και αλγόριθμους αυτομάτων
download (pdf)
Διαλέξεις 7-9 Εισαγωγή στη SPIN
- O model-checker SPIN, η γλώσσα προδιαγραφής συστημάτων Promela, Σημασιολογία εκτέλεσης και παραδείγματα
download (pdf)
Διαλέξεις 10-11 Διακλαδωμένη Χρονική Λογική
- H CTL (σύνταξη και ερμηνεία), διατύπωση ιδιοτήτων, Μοντελοέλεγχος. Δικαιοσυνη
download (pdf)
Διαλέξεις 12-14 Χρονικά Αυτόματα
- Συστήματα πραγματικού χρόνου, διακριτός και συνεχής χρόνος, χρονικά αυτόματα, χρονική CTL.
download (pdf)
Διαλέξεις 15-16 Εισαγωγή στο εργαλείο UPPAAL
- Η γλώσσα του εργαλείου, ο προσομοιωτής, ο μοντελοελεγκτής
download (pdf)
Διαλέξεις 17-18 ’λγεβρες Διεργασιών
- Προδιαγραφή και Επαλήθευση με άλγεβρες διεργασιών. Η άλγεβρα διεργασιών CCS (σύνταξη και σημασιολογία)
download (pdf)
Διαλέξεις 19-20

’λγεβρες Διεργασιών και Σχέσεις Ισοδυναμίας
- Σχέσεις ισοδυναμίας: trace equivalence, failure equivalence, strong bisimulation,  weak bisimulation

download (pdf)
Διάλεξη 21

Aλγεβρες Διεργασιών
- Οι λογικές HML και WHML. Ο λογικός χαρακτηρισμός της ισχυρής και ασθενούς διπροσομοίωσης.

download (pdf)

 
 
 
EPL664
Tutorials
Solutions
Course Schedule
Announcements
Class Contract
Assignments
Related Links

’ννα Φιλίππου, Ιανουάριος 2017