Reference : A formal definition of time in LOTOS
Scientific journals : Article
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/32885
A formal definition of time in LOTOS
English
Léonard, Luc [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques > > > >]
Leduc, Guy mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques >]
1998
Formal Aspects of Computing
Springer Science & Business Media B.V.
10
3
248-266
Yes
International
0934-5043
[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.
Researchers
http://hdl.handle.net/2268/32885
http://www.springerlink.com/content/nvdwr8pmrwvpm8nd/fulltext.pdf

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
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.