ORBi: Leduc Guy - A Timed LOTOS Supporting a Dense Time Domain and Including New Timed Operators

Reference : A Timed LOTOS Supporting a Dense Time Domain and Including New Timed Operators


	Document type :	Scientific congresses and symposiums : Paper published in a book
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/2268/23856

Title :	A Timed LOTOS Supporting a Dense Time Domain and Including New Timed Operators
Language :	English
Author, co-author :	Leduc, Guy [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 > > > >]
Publication date :	Oct-1992
Main document title :	Formal Description Techniques V
Editor :	Diaz, Michel
	Groz, Roland
Publisher :	Elsevier Science
Collection and collection volume :	IFIP Transactions, C-10
Pages :	87-102
On invitation :	No
Audience :	International
Event name :	FORTE 1992
Event date :	13-16 Oct. 1992
Event organizer :	M. Diaz, R. Groz
Event place (city) :	Perros-Guirec
Event country :	France
Abstract :	[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.
Target :	Researchers
Permalink :	http://hdl.handle.net/2268/23856

File(s) associated to this reference

Fulltext file(s):

	File	Commentary	Version	Size	Access
Open access	RUN-PP93-01.pdf		Author postprint	211.45 kB	View/Open

All documents in ORBi are protected by a user license.

Dspace v1.5