A formal definition of time in LOTOS

Enhanced Timed-LOTOS, denoted ET-LOTOS, is an extension of LOTOS that allows the modelling of real-time behaviours. It covers all the aspects of full LOTOS, including data types, it supports both a dense and a discrete time domain and can manipulate time values as any other data values. A tutorial on ET-LOTOS, showing many application examples, has already been published elsewhere. The present paper adds to it by providing an in-depth presentation of its theoretical aspects. The complete semantics is given and explained, and its proper-ties are studied. In particular, we prove that the semantics is consistent and that strong bisimulation is a congruence. This requires to deal carefully with the presence of negative premises in the operational semantics, which are necessary to express urgency. ET-LOTOS is also shown to be a conservative extension of LOTOS for guarded processes, and is the basis of the timed extension of LOTOS currently developed by ISO. To our knowledge, this is the first in-depth study of a language that combines data types and real-time behaviours.