Exercises for the lab classes


  • Session 1

    Modeling a simple system using Hoare's CSP.

    Consider a fault tolerant system, composed by (1) a cheap but unreliable main server, (2) a costly but reliable secondary server, and (3) a front-end that mediates between the client and both servers. The front-end services client requests by forwarding them to the main server. If the main server fails, the secondary server is consulted. So the client does not perceive what server is actually consulted to process its request in the back-end.

    Model this system in CSP and show (using F2R) that it is trace and failure equivalent to the following spec:

    SPEC = request.done.SPEC

    Tools: The FDR2 tool suite. FDR2 is a robust tool for CSP refinement checking freely available for academic use.

  • Session 2

    Modeling a simple system in Milner's CCS.

    Consider the well-known dining philosophers problem, introduced by Dijkstra. Four philosophers are siting around a table. A fork lies down at each philosopher right hand side. Each philosopher alternates between two states: thinking and eating. However, in order to enter into the "eating" state, a philosopher must successfully grab the two forks adjacent to her. After eating, the philospher drops the forks on the table (so that they become again free for use).

    Notice that, in our case with four philosophers, at most two may be concurrently eating.

    Model the system in CCS, representing each philoshoper and each fork by an independent process. The spec of each philosopher and each fork should be esentially the same (up to renaming of actions).

    Analise your system using the MWB. Show that your model may get into deadlock states.

    Modify your spec by introducing an extra component (a coordinator). The cordinator should discipline the access by the clients (the philosophers) to the resources (the fork), so that deadlock is avoided.

    Prove, using the MWB, that your solution is correct (in the sense that no deadlock may occur).

    Specification challenge (for the great students we have)

    Consider the leader election problem: a collection of processes needs to agree, without a centralized control point, which one is to be the leader.

    Model the leader election problem in CCS (consider a small, yet significant, set of processes - say four). Your system must consist in four (essentially equivalent) processes, running in parallel, in order to model a distributed systems. Show, using the MWB, that your solution satisfies the spec:

    LEADER_SPEC = t.'leader_1 + t.'leader_2 + t.'leader_3 + t.'leader_4

    To solve this problem, you may need to do some research in the literature. There are several known solutions to the leader election problem, you must sensible select some algorithm (or devise your own), and model it in CCS, possibly by abstracting away details that would have to be taken into account in a real implementation.

    Tools: The MWB (Mobility Workbench). The MWB is a verification tool for bisimilarity checking, it uses the pi-calculus, not CCS, as modeling language. However, we may see the CCS as a fragment of the pi-calculus, and it is useful to use a common tool for bisimilarity checking both for CCS and for the pi-calculus, that will be studied later on in the course.

  • Session 3

    Modeling a simple system in CCS: communication in a unreliable medium.

    The system contains three components: a SENDER, the MEDIUM, and a RECEIVER. The sender reads messages from the environment and forwards to the MEDIUM. The MEDIUM, may fail to deliver the message to the RECEIVER, or succeed. In the case of failure, the SENDER should retry. Otherwise the message should be forwarded to the RECEIVER, for delivery to the environment.

    Derive a SPEC strongly bisimilar to your SYSTEM. Check with the MWB. Write down the simplest SPEC to which the SYSTEM should be weakly bisimilar. Check with the MWB.

  • Session 4

    Recall Dekker's algorithm. Dekker's algorithm is a lock free solution to enforce mutual exclusion for two threads.

    Model Dekker's algorithm in CCS, and prove, using TAPAs, that it:

    • never allows the two critical sections to overlap in time.
    • never deadlocks
    • is free from starvation
  • Session 4a

    Modeling a digital system: model a full one bit adder using CCS processes to represent individual gates, and verify that it really implements the intended truth table.

    You should use the TAPAs tool to define the system. Check that the system works as expected using hennessy-milner logic.

  • Session 5

    Modeling a system in CCS: access to an object (e.g., a file) in a distributed system.

    A network of nodes compete for accessing a resource. At each moment, only one of the nodes may own the resource. The node (i) that owns the object may signal that condition by issuing a message 'OWN_i.

    At any moment, any node that does not own the resource, may decide to request it. Then, the system must be able to evolve in such a way that the requester object may become the owner. The previous owner will then loose ownership of the resource.

    For a system with three nodes, the SPEC may look like this:

    SPEC = N1()

    agent N1(OWN_1,OWN_2,OWN_3) = 'OWN_1.N1() + t.N2() + t.N3()

    agent N2(OWN_1,OWN_3,OWN_4) = t.N1() + 'OWN_2.N2() + t.N3()

    agent N3(OWN_1,OWN_3,OWN_4) = t.N1() + t.N2() + 'OWN_3.N3()

    In this SPEC, we assume that the node that initially owns the resource is node 1, but this is of course arbitrary.

    Model in CCS a system that is weakly bisimilar (observationally equivalent) to SPEC, but that is implemented as a network of distributed nodes, that may only communicate by message passing.

    Notice that in a distributed system, more than one node may simultaneously request the resource, but only one will get access to it.

    If you prefer, produce first a design in which all nodes are connected to a central coordinator, that arbitrates the access to the resource. But the goal of this exercise is to produce a really distributed implementation, without a centralized controller.

    Verify, using the MWB, that your SYSTEM is weakly bisimilar to SPEC above, and therefore deadlock free.

  • Session 6

    Modeling a dynamic linked system in the Pi-Calculus: the yellowtooth protocol.

    This is a very simplified version of a dynamic linking distributed protocol, similar to the LMP protocol in the Bluetooth protocol stack.

    A set of K nodes is deployed in the environment. After some interactions, the nodes must link themselves in a ring, in such a way that any node may communicate with any other node in the ring. This means that there will be at most K-1 hops in the stable system.

    When finally placed in the ring, each node shares with its two neighbors an uplink (say, to the right) and a downlink (to the left, say).

    Model the system for K = 4 and show that your distributed algorithm is deadlock free, and always converges to a ring shaped topology, using the SLMC tool.

    Challenge: what if we want to model node failure? Would it be easy to accomodate that requirement? What would be the appropriate correctness property of the model?

  • Sessions 7

    In this session we will integrate previous knowledge, and will model several simple cryptographic protocols. Simple security properties will be checked with the Proverif tool.

    • Simple secret distribution.
    • Simple key distribution.
    • Wide Mouthed Frog.
    • Needham-Shroeder and variants.