Lectures Plan

Semantics & Verification, Spring 2006

---

Semester calendar for the course is here.

• Lectures 1-8 are available here.
  
  
• Lecture 9 (10.3.06, 10.15-12.00, B3-104): Timed CCS and Timed Automata [slides] [supplementary]
  
  
  • Plan: Timed labelled transition systems; Timed CSS: syntax and semantics. Timed Automata: syntax and semantics.
  • Reading:
    • Reactive Systems: Modelling, Specification and Verification (Sections 8.1, 8.2, 8.3 and 8.4).
    • Reactive Systems: Modelling, Specification and Verification (Sections 9.1, 9.2).
  • Exercises:
    • 8:15-10:00 in B3-104
    • finishing the work on the first mini project and writing down the report (tutorials will be supervised as usual)
  
  
  
• Lecture 10 (17.3.06, 10.15-12.00, B3-104): Timed and Untimed Equivalences, Region Construction and Hennessy-Milner Logic with Time [slides] [supplementary]
  
  
  • Plan: Timed and Untimed Bisimilarity; Region Construction; Networks of Timed Automata; Hennessy-Milner Logic with Time.
  • Reading:
    • Reactive Systems: Modelling, Specification and Verification (Sections 9.5, 9.6, 9.7).
    • Reactive Systems: Modelling, Specification and Verification (Sections 10.1).
    • Secondary Reading (results only) Reactive Systems: Modelling, Specification and Verification (Sections 9.3, 9.4, 10.2).
  • Exercises:
    • 8:15-10:00 in B3-104
    • [Exercise Set 9] [Solutions]
  
  
  
• Lecture 11 (22.3.06, 10.15-12.00, B3-104): Timed Automata and UPPAAL [slides] [slides 3x2]
  
  
  • Plan: Introduction to UPPAAL; Modelling, specification, simulation and verification in UPPAAL; practical examples.
  • Reading:
    • A Tutorial on UPPAAL
    • Timed Automata: Semantics, Algorithms and Tools (sections 3.1, 5.2 and the part about networks of timed auotmata in 5.1)
  • Exercises:
    • 8:15-10:00 in B3-104
    • [Exercise Set 10] [Solutions]
  
  
  
• Lecture 12 (24.3.06, 10.15-12.00, KS3 1.104): Mini Project: Gossiping Girls in UPPAAL
  
  
  • Plan: to solve in groups the mini project (the description is here); we will be available in the lecture rooms E3-209, E3-109 plus neighbouring group rooms the whole morning to assist you; make sure that you have one laptop for each working group and that you are able to run UPPAAL.
  • Reading:
    • A Tutorial on UPPAAL
  
  
  
• Lecture 13 (5.3.06, 10.15-12.00, KS3 4.110!!!): Binary Decision Diagrams [slides] [slides 3x2]
  
  
  • Plan: Boolean expressions; normal forms; Shannon's expansion law; ordered and reduced binary decision diagrams; canonicity lemma; algorithms for manipulating BDDs.
  • Reading:
    • An Introduction to Binary Decision Diagrams (pages 6-27)
  • Exercises:
    • 8:15-10:00 KS3 4.110 (finish mini project 2).
    • Finish the work on the second mini project and writing down the report (we will supervise this as usual).
  
  
  
• Lecture 14 (7.4.06, 10.15-12.00): Application of Binary Decision Diagrams [slides] [slides 3x2]
  
  
  • Plan: ROBDDs and constraint solving; Boolean encoding of transition systems; bisimulation checking and model checking; IBEN
  • Reading:
    • An Introduction to Binary Decision Diagrams (pages 27-34)
    • Practical Verification of Embedded Software
    • A SAT Solver Primer(optional but very interesting reading)
  • Exercises:
    • 8:15-10:00 in B3-104
    • [Exercise Set 13] [Solutions]
  
  
  
• Lecture 15 (21.4.2005, 10.15-12.00, B3-104): Round-up of the Course [slides] [slides 3x2] [print-friendly 3x2]
  
  
  • Plan: Overview of key topics of the course; information about the exam and its form; selection of the star exercises. The lecture will be given by Jiri Srba.
  • Exercises:
    • 8:15-10:00 in B3-104
    • Remember to bring one laptop per each group, we will be experimenting with the tool Iben. Some information about the tool and a link to a very short tutorial is on this page.
    • Exercises:
      • 8:15-10:00 in B3-104
      • [Exercise Set 14] [Sudoku in Iben]