University of Ottawa
SEG-2106 : Software construction
Gregor v. Bochmann

SEG-2106 - Lab-2


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

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.

Part 3: The telephone system example

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.