Project Statement

The objective of the project is to define and analyze a model of a distributed leader election algorithm.

Consider:

  • a) Use a symmetric network: all nodes run the same "code", and initially are not aware of the size of the network.
  • b) Your approach must work for networks with any number of nodes (greater than one).
Work out the model in the pi-calculus and the SLMC.

Fornalize and check the following properties:

  • 1) only one node gets elected.
  • 2) some node gets elected ( the system always converges towards a solution)
  • 3) upon termination, all nodes get to "know" what node was elected.
Check your model for systems with 2, 4 and 5 nodes using SLMC.

Argue that your algorithm is correct for any number of nodes.

Deliverables:

  • Source code of the SLMC spec.
  • Summary report (1-3 pages), explaing the solution.
Challenge for EXTRA CREDIT

For extra credit, write down a model where initially all nodes are isolated and disconnected from each other, and only share one public channel.