Playing with the LTSA tool (modeling state machines communicating by rendezvous)

An introduction to the LTSA tool and its use (see example in file "check properties") was discussed in class. An explanation of the syntax of the language used to write LTS model specifications acceptable by the LTSA tool is given here.

Part 1: Revision

• Task (A): Go through the examples included in the "check properties" file and execute the corresponding LTSA commands to verify your understanding of the operations of LTSA.

Part 2: The Hotel example

Please load the Hotel example (example file "hotel-room-and-restaurant-3") into LTSA. Look at the state machine diagrams of the different system component and of the global system behavior. Perform some simulated executions by using the command Check -> Run.

• Task (B): Check whether the test sequence (1) through (4) are executable by the model. To see result of the composition of the SYSTEM with Sequence_1, you must select in the selection bar over the drawing window the selection TEST_1 (instead of the selection SYSTEM used earlier).
  • Explain what happens in cases of problems. Do you think that the specification of the model should be changed in order to realize the test sequences (which are supposed to be the use cases of the requirements), or is there an error in the use cases ? - Please explain.
• Task (C): Modify the Hotel example (version 3) in such a manner that the hotel client must eat in the restaurant before he can check out.
  • Step 1: think about how you can solve this problem, what changes should be introduced into the specification of the different state machines (make as few changes as possible).
  • Step 2: make the changes in the specification and compile it.
  • Step 3: compose the system and check that it satisfies the requirements above (for instance, by looking at the global state diagram and by checking that there is no deadlock)
  • Question C: (a) explain the changes made and why, (b) show the changed specification, (c) explain the verifications performed.

Part 3: The telephone system example

• Task (D): Load the telephone-system example into the LTSA tool
  • Step 1: Read the text defining the telephone system and the test cases. Compile the system (commands build -> parse; build -> compile). Look at the transition diagrams for the three system components (click on DRAW; then select each of the components in the left window); play with the size of the diagrams by clicking on the funny symbols between the left window and the window showing the diagrams.
    • Check that the diagrams make sense - do you think the specification defines a suitable behavior for these three components ?
    • Question D.1: The state called WAIT in the the behavior definition of PHONE1, what is the state number by which this state is represented in the state diagram generated by the LTSA tool ? - Similarly, for the state TALKING1, and the state BUSY of the PHONE2 behavior ?
    • Use the animator of the tool to perform some simulated execution of the telephone system (command check -> run ). The animator shows which interactions are enabled (are possible to be executed) in the current state of the system. Initially, each user may pick up the phone.
    • Build the composition of the three components (command build -> compose); look at the global behavior diagram of this composition, called PHONE_SYSTEM (click on DRAW again). Does this behavior make sense ?
  • Now we want to check whether certain execution sequences can be realized by the given specification of the PHONE_SYSTEM. For this purpose we combine the PHONE_SYSTEM with an execution sequence and call this composition a TEST. The text of the specification contains three such execution sequences and corresponding tests, called TEST1, TEST2 and TEST3. To see what results from the composition of the PHONE_SYSTEM with Sequence_1, you must select in the selection bar over the drawing window the selection TEST1 (instead of the selection PHONE_SYSTEM used earlier); then perform the composition command, and have a look at the resulting diagram. You will see the whole sequence Sequence_1 up to the end, which means that it can be realized by the PHONE_SYSTEM.
  • Do the same for TEST2.
  • Do the same for TEST3.
    • Question D.2: why is this sequence not realizable (it stops in the middle) ?
  • Play with other execution sequences, by defining your own Sequence_4 and TEST4, similar as the given examples.
  • Answer the following questions:
    • Question D.3: What will happen when the users of both phones first do the pick-up and then the user of PHONE1 dials while the user of PHONE2 hangs up ? - Use the LTSA tool to find out.
    • Question D.4: By what sequences could you model the case that the users of both phones do the pick-up simultaneously ? (How are simultaneous interactions modelled with the LTS formalism which uses rendezvous ?) - Similarly, for the simultaneous hang-up done by both users simultaneously ?
  • An abstract view, called "Abstract" is defined at the bottom of the text. Please check whether this abstract view is realized by the given model.
    • Question D.5: What is the meaning of this property ? - Why is it realized ?
    • Question D.6: Can you find other interesting abstract properties ? - If yes, define such a property and add it to the LTSA specification. Check whether your property is satisfied by the given model.
  • There is a bug in this behavior description of the phone system, namely, when the user of PHONE2 initially picks up the phone and goes into the busy state, the PHONE2 cannot exit this state until it is called by PHONE1 and they both hang up jointly (this is so, because the hang_up interaction is in rendezvous between the two phones, and one phone cannot do it alone).
    • Question D.7: Modify the specification of this model in order to allow the two users to hang-up correctly in the situation when a connection was made and in the case that User2 was busy. The specification should be such that the SWITCH also knows when the connection is terminated. Suggestion: introduce two different hang-up interactions.
      • Analyse the safety of your specification.
      • Write some execution sequences (similar to those given for the original specification) which represent some typical use cases for the correct termination of the connection provided by your modified system specification.

Results to be handed in

This is an "informal" Lab. At the end of the Lab session, please show to the TA your draft texts and diagrams that you prepared for the work items (A) through (D). 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.