Lab-4 - SEG-2106 - Verification of concurrent systems

Part A: Exercise in performing reachability analysis on paper

We consider two state machines with the behavior shown in the diagram below. They communicate with one another by asynchronous message passing and FIFO input queues. The exchanged messages are labelled a, b, c, d and e.


Your tasks:

  1. Please, perform a reachability analysis in order to explore the behavior of the global system which consists of these two interacting state machines. Draw the reachable global states and the transitions that lead to them (using the notation introduced in the course notes).
  2. Identify any design problems that are encountered (such as non-specified receptions or deadlocks)
  3. For each problem identified, explain a possible solution by indicating changes to the above specifications that you suggest. If you have time, verify that the proposed solutions lead to a system specification without problems.

Things to prepare:

Part B: Analyzing some further versions of TCP with LTSA

We start out with Version 4 of the LTSA spécification of TCP, as discussed in the course notes. Your tasks are the following:

Your tasks:

  1. Modify the TCP specification in order to realize the service interactions according to the OSI paradigm shown in Figure (b) of the course notes: Version 5
  2. Include the disconnection phase (as shown in the Wikipedia diagram): Version 6
  3. Include simplified data transfer by assuming that user data is sent by data messages between the two parties.

Results to be handed in

This is an "informal" Lab. At the end of the Lab session, please show to the TA your reachability graph and LTSA models and diagrams that you prepared for this lab. The TA will take note of the completeness of your work, but will not evaluate the quality of your work.

Please consult with the TA during the Lab session. The role of the TA is to help you to do the work suggested within this Lab.

Last update: February 3, 2015