Abstract:

Formal description techniques based on process algebras allow the precise and succinct description of complex reactive systems. Such specifications are concise and unambiguous but are sometimes difficult to understand. Tools like animators are then useful for the correct understanding and the design of a specification. An animator allows the step by step execution of the system description in order to insure that what is formally described is really what was desired. This allows the detection of design errors at early stages of the system development. We have developed a tool called SELTA (for Simulator of ET-LOTOS based on Timed Automaton) which allows the animation of ET-LOTOS specifications. ET-LOTOS is a timed extension of the formal description technique LOTOS. This language allows the specification of real-time systems where timing evolution can modify the behavior of the system. This timed extension is currently considered by the ISO work-group dedicated to the revision of the LOTOS standard (E-LOTOS). The tool supports all the ET-LOTOS operators. The data part has not been implemented, only the rational data type can be used. SELTA allows the animation of the specification by offering to the user the possible evolutions of the system. At each step, the user must choose between the firing of an enabled action and the timed evolution of the system. The animator supplies information to the user at each step:

• The elapsed time since the beginning of the animation.
• The maximal possible progress in time of the currently animated behavior. This information shows that an action is urgent (Internal actions are urgent in ET-LOTOS).
• The next important moment in the system's life. The tool can determine the amount of time by which the system must age to change the set of enabled actions.