LTS-Analyser (TLSA) - un outil simple et utile pour l'analyse de systèmes à transitions étiquettées

Cet outil a été développé en Grand-Bretagne pour apporter un support pratique pour la modélisation de systèmes concurrents. Il a été utilisé pour les exemples dans le livre "Concurrency: State Models and Java Programs".

Il y a la version originale, tres simple (que j'utilise dans le cours), qui vient comme applet en Java (ou peut être copiée d'ici). Une nouvelle version a été intégré dans l'environnement Eclipse et a essentiellement les mêmes fonctionalités (download ici). La version Eclipse a aussi un peu de documentation: un help-guide qui contient un appendice A avec un Quick Reference Guide. Dans ce cours, nous n'utilisons qu'un nombre restreint de fonctionalités, et vous allez comprendre les pluparts des aspects en regardant les examples donnés dans le cours.

Tous les exemples LTSA utilisés dans SEG-2506 se trouvent ici.

Mini-Introduction to the syntax of LTSA model descriptions (à traduire en français)

We use the example of the hotel system to explain the basic features of LTSA. Here is the text of this example:

// state machine of the client: it has only one state, all client actions are possible any time.
CLIENT = (checkIn -> CLIENT | checkOut -> CLIENT |
eat -> CLIENT | payCash -> CLIENT | chargeRoom -> CLIENT).

// state machine of a restaurant. The alphabet of this LTS is {eat, payCash, chargeRoom}
RESTAURANT = (eat -> DONE),
DONE = (payCash -> RESTAURANT | chargeRoom -> RESTAURANT).

// state machine of a room. The alphabet of this LTS is {checkIn, checkOut, chargeRoom}
ROOM = (checkIn -> OCCUPIED),
OCCUPIED = (checkOut -> ROOM | chargeRoom -> OCCUPIED).

ROOM2 = (checkIn -> checkOut -> ROOM2).

// The system consists of one client, one restaurant and one room
||SYSTEM = (CLIENT || RESTAURANT || ROOM).
// List of interactions in this system:
// (a) Rendezvous involving the CLIENT and the RESTAURANT: eat, payCash
// (b) Rendezvous involving the CLIENT and the ROOM: checkIn, checkOut
// (c) Rendezvous involving all three objects: chargeRoom

As the last line indicates, the system consists of three state machines that work concurrently. Working concurrently, means that transitions of different state machines that have the same name can only be execute jointly, that is, in rendezvous.

The first two lines define the state machine CLIENT. CLIENT is the name of the state machine and also the name of its initial state. All state names are written in upper case characters. The CLIENT machine has only one state. The words in lower case characters are transition names. The first line indicates that from the CLIENT state, the machine can make a checkIn transition which leads to the next state CLIENT, or a check-out transition that leads to the same state. Etc. The definition of state machine is terminated by a dot "."

The RESTAURANT state machine has two states, the initial state RESTAURANT and another state called DONE.The first line of its definition indicates that from the initial state, there is only one transition named eat. The second line defines the transitions available from the state DONE. Note that all transitions from a given state are put in paranthesis, followed by a comma "," if this is not the last state of the machine definition.

Note that some of the states of a state machine may not be explicitely mentioned (they have no name). For instance, the definition of the ROOM2 state machine has two states: ROOM2 and the state reached after the transition checkIn. This second state is in-between the transitions checkIn and the following checkOut. After checkOut, the machine is again in its initial state ROOM2.

Note: It is important to note for each state machine the set of transition names, which is called the "alphabet" of the machine. It is the set of interactions in which it participates. If there is an intersection between the alphabets of two (or more) machines, then the transitions with these names can only be executed in rendezvous. A transition with a name that is unique to the given machine, is executed independently of the other machines within the system. For instance, the transition eat is performed by RESTAURANT independently of other machines, check-in is performed by CLIENT and ROOM in rendezvous, and chargeRoom is executed in rendezvous by all three machines (and it can only occur if all three machines are in a respective state where this transition is allowed).

Mini-Introduction to the commands of the LTSA tool

The LTSA tool has the drop-down menues File, Edit, Check, Build, Window, Help and Options. Below are three buttons: Edit, Output, and Draw. A typical steps of using the tool are the following:

1. Use the editing functions to create a model definition.
2. Use the commands Build -> Parse and Build -> Compile to create in internal representation of the model for further processing.
3. View the graphic representation of the state machines included in your model by clicking on Draw and then clicking on the name of the state machine you what to visualize. Note that the graphical representation does not include the state names of your model (since these names have no semantic meaning, that is, they can be changed without changing the meaning of the model)
4. In the textual field "Target Composition" of the tool, select the composition that you would like to simulate. Note, the hotel model contains only one composition, the one that is called SYSTEM. The syntax for the definition of a composition is a composition name preceeded by "||" and at the right side the names of the state machines (separated by "||" ) that should be executed concurrently. In the case of the hotel example, the SYSTEM is already selected by the tool.
5. Execute the command Build -> Compose, which builds a global model of these state machines running concurrently with rendezvous interactions.
6. View the graphic representation of the composition.
7. Use the command Check-> Run to perform a interactive simulation of the composed system. During the execution, you may look at the graphical representation of each machine, or the global system. A stats in red is the current states of the machine.
8. Use the command Check -> Safety to check whether there is the possibility that the composed system may enter a blocking state (a state without any transition), called a deadlock.

Verification options in LTSA

• Deadlock: LTSA checks whether a composed system as a deadlock. A state in a single component that has no transition is considered an Error state. A state with name END is considered the normal end state of a behavior.
• Test sequences: One can define a sequence of interactions and compose this sequence with the system specification. If there is a deadlock, the test sequence cannot be performed by the specified system.
  • Attention: The sequence may have a smaller alphabet than the system. In this case, interactions not in the sequence alphabet may be interspersed in the sequence at any point.
  • Examples are given in the Hotel V3 example.
• Safeness properties: Using the keyword property, one may define a behavior and compose it with the system. This composition checks that all possible execution sequences of the system (when projected onto the alphabet of the property behavior) are allowed sequences according to the property. Note: The property is usually a more abstract view of the system behavior, for instance the service specification of a protocol system.
  • Examples are given in the Hotel V3 example.