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 |
Spain |
Tel: +34 1 5495700 Ext 442 |
Fax: +34 1 3367333 |
E-mail: grabay@dit.upm.es |
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:http://www.dit.upm.es/~grabay/
This Page was prepared by Mark Jorgensen.