Abstract:ELOTOS is an extension of protocol specification language LOTOS which is an ISO standard. In this paper, the authors try to give the semantics of ELOTOS by defining a derivation system (like LOTOS).Then, from LTS (labeled transition system ) of restricted ELOTOS, they construct the TFSM(trace finite state machine) for trace semantics, and TFSM is a kind of performance evaluation model.