i636 Specification and Verification of Distributed Systems

Lecturers: OGATA, Kazuhiro & FUTATSUGI, Kokichi
Room: I2
Term 2-2, 2008

News

- Jan 06: A mistake on page 11 of lecture note 4 is corrected.
- Dec 16: The problem of Assignment is available.
- Dec 01: This web site is open.

Examination

- Feb 10, Tuseday, 09:20-10:50
Problems
Solutions
Full marks: 35, Highest: 24, Average: 17

Assignment

Send your solutions to the lecturer by email.
- Assignment (deadline: Around Feb 16; Note that the deadline may have to be shortened!) 
  List of those who have submitted their solutions
 

Lecture Schedule

1.  Dec 04, 11:00-12:30: lectureNote1 Outline of How to Analyze Systems with Maude
2.  Dec 09, 09:20-10:50: lectureNote2 Functional Modules
3.  Dec 11, 11:00-12:30: lectureNote3 Term Rewriting Systems
4.  Dec 16, 09:20-10:50: lectureNote4 System Modules
5.  Dec 18, 11:00-12:30: lectureNote5 Invariant Verification with Search
6.  Jan 08, 11:00-12:30: lectureNote6 LTL Model Checking
7.  Jan 13, 09:20-10:50: lectureNote7 Suzuki-Kasami Distributed Mutual Exclusion Protocol (1)
8.  Jan 15, 11:00-12:30: lectureNote8 Suzuki-Kasami Distributed Mutual Exclusion Protocol (2)
9.  Jan 20, 09:20-10:50: lectureNote9 Needham-Schroeder Public-Key Authentication Protocol (1)
10. Jan 22, 11:00-12:30: lectureNote10 Needham-Schroeder Public-Key Authentication Protocol (2)
11. Jan 27, 09:20-10:50: lectureNote11 Alternating Bit Protocol (1)
12. Jan 29, 11:00-12:30: lectureNote12 Alternating Bit Protocol (2)
13. Feb 03, 09:00-10:50: lectureNote13 Proof Score Approach to Verification
14. Feb 05, 11:00-12:30: lectureNote14 Induction Guided Falsification

Specifications Used in the Course

1. qlock0.maude, qlock1.maude, qlock2.maude, qlock3.maude
2. spec2.maude, table1.maude, table2.maude, table3.maude, table4.maude
3. spec3.maude
4. spec4.maude
5. spec5.maude
6. spec6.maude
7. ots-sk.maude
8. sk.maude, sk1.maude, sk2.maude, sk3.maude
9. ots-nspk.maude
10. nspk.maude, nslpk.maude, nslpk1.maude
11. ots-abp.maude
12. abp.maude, abp1.maude, abp2.maude, abp3.maude, abp4.maude
13. ots-ticket.maude, ots-ticket-invariants.maude, ots-ticket-proof1.maude, ots-ticket-proof2.maude, ots-ticket-proof3.maude, ots-ticket-proof4.maude, ots-ticket-proof5.maude, ots-ticket-proof3-old.maude, ots-ticket-proof4-old.maude, ots-ticket-proof4-old2.maude
14. ots-nspk.maude, ots-nspk-invariants.maude, ots-nspk-proof1.maude, nspk1.maude

Evaluation 

One assignment (65%) & one examination (35%).

References

1. Manuel Clavel, et al.: All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic, LNCS 4350, Springer, 2007.
A preliminary version is available at the Maude web site.
2. The Maude webpage: http://maude.cs.uiuc.edu/
3. Nancy A. Lynch: Distributed Algorithms, Morgan Kaufmann, 1997.
4. Leslie Lamport: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley, 2002.

The Maude System

- The latest version for Linux & MacOSX is available at the Maude web site.
- Maude for Windows is available at the MOMENT project web site.