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:

• Sketch of a global reachability graph for the system specification given above.
• Short text concerning points 2 and 3 above (and a second reachability graph if you had time to do it)

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
• Eliminate the service primitives Connect and Listen (already eliminated) and introduce the primitives shown in Figure (b) at the appropriate states of the state machine. This becomes Version 5. Verify that there is no deadlock.
• Define a new version of the Check_Service property and verify that it holds for the system specification Version 5.
2. Include the disconnection phase (as shown in the Wikipedia diagram): Version 6
• After the data exchange phase (state Established), include the disconnection phase, as described by the Wikipedia diagram. Notes:
  • CLOSE is a service primitive performed by a user to indicate that he wants to terminate the connection. After this primitive, the user should not send any data any more, but he may still receive data sent from the other side.
  • fin is a type of message, indicating that the sending user wants to terminate the connection. The fin message will be acknowledged by an ack. This is similar to connection establishment.
3. Include simplified data transfer by assuming that user data is sent by data messages between the two parties.
• In TCP, data transmission may start in the Established state and may continue until a CLOSE service primitive occurs. This means that data reception may occur in these states, but also in some other states during the disconnection phase. The prupose of this taks is to introduce data sending transitions (leading back to the current state) when this is allowed, and to check in which states these data messages may still be received. For this purpose, you should introduce data reception transitions in those states where data reception may occur (transitions leading back to the same state). If you can eliminate the data reception transition in a given state of the disconnection phase without introducing the problem of deadlock, then this shows that data may never be received in that state.
• Step 1: Introduce data sending and receiving transitions as explained above. Introduce receiving transitions in all states of the disconnection phase. This becomes Version 7. Show that there is no deadlock in Version 7.
• Step 2: For each of the states of the disconnection phase, eliminate the receiving transition and check for deadlock. If there is no deadlock introduced, then no data message will be received in this state.
• Result: Which are the states where no data will be received with TCP ??

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.