next up previous

Final Report of the COST-247 Action

State Exploration in TE-LOTOS with Time Extended LOLA

Gualberto Rabay Filho1

Dept. Ingenieria de Sistemas Telematicos
Universidad Politecnica de Madrid
ETSI Telecomunicacion
E-28040 Madrid
Tel: +34 1 5495700 Ext 442
Fax: +34 1 3367333


TE-LOLA (Timed Extended Lotos LAboratory) is a software prototype that supports full TE-LOTOS according to the current ISO working group proposal. TE-LOLA's functionality includes: Expansion (EFSM generation), Parameterized Expansion, Interleaved Expansion, Timed Testing and Timed Simulation/Debugging. This presentation explains relevant issues regarding state exploration in TE-LOTOS. The analysis of timed LOTOS specifications is more complex than the untimed one for many reasons. First, it is necessary to carry out extra functions (intersection of time intervals of participating actions in synchronizations, implementation of aging, urgency action pruning, etc.. ). Second, the generated state space is almost always much bigger due to the generation of time variables in the aging process, even considering elimination of states that violate time constraints. And third, interval time constraints induce a heavy and complicated symbolic computation not easy to deal with formally.

This presentation has been given during the COST-247 7th Management Committee Meeting (Madrid, Spain, February, 12--13, 1995).

COST-247 Working Group(s): 1

Web Link:

1 On leave from TELEBRAS, Brasil

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page