Assignment

1. Read one of the following papers:

[1] Glenn Ricart, Ashok K. Agrawala: An optimal algorithm for mutual exclusion in computer networks, Communication of the ACM, 24(1): 9-17, 1981.
[2] K. Mani Chandy, Leslie Lamport: Distributed snapshots: determining global states of distributed systems, AMC Transactions on Computer Systems, 3(1): 63-75, 1985.

Or propose a paper you are going to read to the lecturer (ogata); if the lecturer accepts the proposal, read the paper.

2. Describe a system (or protocol) found in the paper, including some properties the system should satisfy.

3. Make an OTS modeling the system (or protocol).
It is optional to write equations defining transitions. Your score is not reduced even if you do not write such equations. But, such equations will be evaluated positively.

4. Write a specification of the OTS in Maude.

5. Model check that the OTS satisfies the properties with command search and/or the LTL model checker.

6. Write a report that describes the system, the properties, the OTS, the specification, the experiments (model checking), etc.

7. Send your report and specification(s) to the lecturer (ogata) by email as attachments.
The subject of the email should be [i636-assignment], and your name and student ID should be explicitly written in the report. A preferable format of reports is pdf. Ask the lecturer for other formats.

The following papers may help you do the assignment:

[A] Kazuhiro Ogata, Kokichi Futatsugi: Formally Modeling and Verifying Ricart&Agrawala Distributed Mutual Exclusion Algorithm, Proceedings of the 2nd Asia-Pacific Conference on Quality Software  (APAQS'01), IEEE Computer Society Press, pp.357-366 (2001).
[B] Kazuhiro Ogata, Kokichi Futatsugi: Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm, IEICE TRANSACTIONS on Fundamental of Electronics, Communications and Computer Science, E90-A(8): 1690-1703, IEICE, 2007.