|Final Report of the COST-247 Action|
Animation of real-time ET-LOTOS specifications
Christian Hernalsteen and Antony De Jacquier
|Universite Libre de Bruxelles|
|Departement d'Informatique, CP212|
|Bl. du Triomphe|
|tel: +32 2 650 50 42|
|fax: +32 2 650 56 09|
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:
This presentation has been given during the COST-247 9th Management Committee Meeting (Antalya, Turkey, November 4--5, 1996).
COST-247 Working Group(s):
This Page was prepared by Mark Jorgensen.