Verification of Complex Systems (2010/2011)

Announcements

• May 28. The project description is online.
  
  
• April 8. Next week there will be two invited lectures by Dr. Franco Raimondi:
  • Monday, April 11th, from 16.00 to 18.00
  • Wednesday, April 13th, from 9.30 to 11.30
  
  
  
• March 10. A mailing list for this class is now active. It will be used to handle project deadlines and further notices. Please send me an email to subscribe to the list.
  
  
• March 7. The course on Verification of Complex Systems is a module of 6 credits inside the integrated course on Formal Methods and Verification that will be taught in English.
  
  

Timetable

• Thursday: 14:30-18:00; room 1.7

Lecture Notes

• Lecture Slides on UPMurphi
• Lecture Slides on PDDL+ (Many thanks to Maria Fox)
• Lecture Slides on HyTech
• Lecture Slides on Modelling System Properties
• Lecture Slides on Timed Automata
• Lecture Slides on CTL Model Checking PART 1 (many thanks to Dr. Franco Raimondi)
• Lecture Slides on CTL Model Checking PART 2 (many thanks to Dr. Franco Raimondi)
• Lecture Slides on CMurphi
• Lecture Slides on Automata-based Modelling (PART 2)
• Lecture Slides on Automata-based Modelling (PART 1)

Tools, Case Studies and Suggested Readings

CMurphi

• CMurphi 5.4.3 (download)
• Script compile (download)
• Peterson's algorithm for N-processes mutual exclusion (download the CMurphi model)

---

UPPAAL

• Uppaal webpage

---

HyTech

• HyTech homepage
• Train-gate controller: Linear Hybrid Automata (download)
• Train-gate controller: HyTech Verification Model (download)
• Train-gate controller: Hytech Parametric Analysis Model (download)

---

SPIN

• SPIN homepage
• An overview of SPIN (with some verification examples) (download pdf).

Project

• Project Description (pdf)
  
  
• Metric-FF homepage
• POPF homepage