Abstract:

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.