|
| 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 |
| e-mail: chernals@ulb.ac.be |
| 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