next up previous

Final Report of the COST-247 Action

Transformation of ET-LOTOS Processes in Extended Timed Automata

Christian Hernalsteen

Universite Libre de Bruxelles
Departement d'Informatique, CP212
Bl. du Triomphe
Brussels, Belgium
tel: +32 2 650 50 42
fax: +32 2 650 56 09


We propose to define a framework to verify TCTL formulas on ET-LOTOS specification. The first step is to define an extended timed automaton in which ET-LOTOS will be transformed. This intermediate representation will be more easy to handle for the verification of TCTL formulas. The timed automaton is extended with variables. The transformation of all the ET-LOTOS operators (except the generalized choice) has been defined including the process instantiation. The idea is to develop a method to verify TCTL formulas on this extended timed automaton. This part will be undertaken in a near future.

This presentation has been given during the COST-247 5th Management Committee Meeting (Warsaw, Poland, June 12--13, 1995).

COST-247 Working Group(s): 1

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page