Reference : A formal definition of time in LOTOS
Scientific journals : Article
Engineering, computing & technology : Computer science
A formal definition of time in LOTOS
Léonard, Luc [Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques > > > >]
Leduc, Guy mailto [Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques >]
Formal Aspects of Computing
Springer Science & Business Media B.V.
Yes (verified by ORBi)
[en] operational semantics ; real-time
[en] 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.

File(s) associated to this reference

Fulltext file(s):

Restricted access
RUN-PP98-04.pdfNo commentaryPublisher postprint173.91 kBRequest copy

Additional material(s):

File Commentary Size Access
Open access
RUN-PP98-05.pdfFull version of the paper with all the proofs479.86 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.