Reference : A Timed LOTOS Supporting a Dense Time Domain and Including New Timed Operators
Scientific congresses and symposiums : Paper published in a book
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/23856
A Timed LOTOS Supporting a Dense Time Domain and Including New Timed Operators
English
Leduc, Guy mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques >]
Léonard, Luc [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques > > > >]
Oct-1992
Formal Description Techniques V
Diaz, Michel
Groz, Roland
Elsevier Science
IFIP Transactions, C-10
87-102
Yes
No
International
FORTE 1992
13-16 Oct. 1992
M. Diaz, R. Groz
Perros-Guirec
France
[en] A time extended version of LOTOS, denoted Timed LOTOS, is proposed for the modelling of quantitative timed behaviours. In this language neither the syntax nor the semantics are restricted to a specific time domain, i.e. a dense time domain is supported as well. Timed LOTOS incorporates a notion of urgency which is restricted to the internal actions. This is usually referred to as the maximal progress or minimum delay property. Timed LOTOS processes have also some pleasing properties such as the deadlock freeness property (i.e. processes can never stop the progression of time), and the persistency property (i.e. by idling, a process will not lose any capability of performing an action). In Timed LOTOS the delay operator is powerful because it allows the specification of a time interval in which the delay is nonderministically chosen. Two other powerful timed operators are defined which allow the expression of timed constraints on interactions, i.e. on actions involving several processes. The first one introduces a delay before the execution of any instance of a given action in a process. A second operator allows to start a time-out on any instance of a given action in a process, and to activate another process when such a time-out expires. The originality of these two operators is that they constrain interactions between processes, and support adequately a structured specification style.
Researchers
http://hdl.handle.net/2268/23856

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
RUN-PP93-01.pdfAuthor postprint211.45 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.