Research in LOTOS Animation

LOTOS specification Execution Animation

LOTOS is a Formal Description Technique (FDT) for the specification of temporal ordering of events. It is an algebra and has a number of operations like sequence, choice, parallelism (synchronization and interleave). It can be used at all steps in the life cycle from design to implementation of telecommunication system. But the most important aspect is that a LOTOS specification can be executed allowing the analyst to explore the alternate behaviors a system can have and thus detect faults early in the development process and avoid costly implementation overhauls. The Execution of LOTOS specifications can be performed with a variety of tools that are all text based, i.e. produce listings. This project was about providing graphical animation capabilities so as to allow the designer to visualize a particular behavior.

The LOLA_win tool

This is an extension of the Universidad de Madrid-DIT tool LOLA. A number of configuration files enables the designer to map LOTOS components to graphic objects and thus produce an animation. A list box displays the next possible events that could occur in a given state. There are two ways to explore the state space, one with a single click on an event in the event list box will merely draw an array between the participating component, the other with a double click will execute the event and move the system into the next state and display the corresponding possible events in that given state.

Some graphic object, like the telephones in the above example can be associated to a virtual terminal that has a keypad and feature keys. These virtual terminals can be used to execute events in the list box providing that they are related to a key.

The LOTOS to MSC transformation tool

This tool enables to transform a LOTOS execution trace to a Message Sequence Chart (MSC). The input is a LOTOS trace file generated by LOLA, the results is an MSC mpr file that can be used with the Telelogic Tau/MSC tool for display.

A LOTOS specification example
A LOTOS execution example
A LOTOS execution Trace example
A LOTOS Trace converted to MSC textual notation example
A LOTOS Trace converted to MSC graph example