References of "Leduc, Guy"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailA Timed LOTOS Supporting a Dense Time Domain and Including New Timed Operators
Leduc, Guy ULg; Léonard, Luc

in Diaz, Michel; Groz, Roland (Eds.) Formal Description Techniques V (1992, October)

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 ... [more ▼]

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. [less ▲]

Detailed reference viewed: 20 (2 ULg)
Full Text
Peer Reviewed
See detailA Framework Based on Implementation Relations for Implementing LOTOS Specifications
Leduc, Guy ULg

in Computer Networks & ISDN Systems (1992), 25(1), 23-41

A framework is developed for studying the implementation process, as a stepwise process in which an abstract specification is successively transformed to reach a final compilable specification adapted to ... [more ▼]

A framework is developed for studying the implementation process, as a stepwise process in which an abstract specification is successively transformed to reach a final compilable specification adapted to the computer environment. In this context, an implementation relation is referred to as the relation which should link any ``valid'' implementation to its abstract formal specification. In other words, the implementation relation is intended to express formally the notion of validity. Our framework allows the exact characterization of the transformations which may take place at each step for a given implementation relation. This framework is essential for dealing with non-transitive implementation relations. In the second part of the paper, these results are exemplified in LOTOS on some existing relations, and an apparent paradox is presented. Some new results about these relations are also derived. [less ▲]

Detailed reference viewed: 13 (0 ULg)
See detailOSI 95 Enhanced Transport Facilities and Functions
Baguette, Yves; Léonard, Luc; Leduc, Guy ULg et al

Report (1992)

Detailed reference viewed: 11 (2 ULg)
Full Text
Peer Reviewed
See detailAn Upward Compatible Timed Extension to LOTOS
Leduc, Guy ULg

in Parther, Ken; Rose, Gordon (Eds.) Formal Description Techniques IV (1992)

We propose a timed extension of LOTOS, denoted TLOTOS, which is upward compatible with the standard LOTOS. It means first that a timed behaviour expression which does not use any language extension will ... [more ▼]

We propose a timed extension of LOTOS, denoted TLOTOS, which is upward compatible with the standard LOTOS. It means first that a timed behaviour expression which does not use any language extension will have the same semantics as in standard LOTOS. In addition, we have pushed this upward compatibility one step beyond by requiring and obtaining that all the familiar equivalence laws of standard LOTOS be preserved e.g. B [] B approximately B, B [] stop approximately B. This is needed in order to keep the intuition of a standard LOTOS user unchanged. TLOTOS has been mainly inspired by other approaches such as Moller Tofts's TCCS (Temporal CCS), Hennessy Regan's TPL (Temporal Process Language) and Nicollin Sifakis's ATP (Algebra of Timed Processes). Our model is not strictly asynchronous (like standard LOTOS, CCS, CSP, ACP) nor strictly synchronous (like SCCS, CIRCAL, Meije). For compatibility and simplicity, we decided to keep the model asynchronous for a large part and, for dealing with time, to introduce a `'synchronous part'' by way of a new basic `'synchronous'' or timed action in the asynchronous semantic model. The design of our TLOTOS is presented together with other possible design alternatives which are all rejected according to our compatibility or expressive power requirements. The solution that we obtain is simple and satifactory, and its operational semantics is presented in depth. Two examples are provided to illustrate the use of TLOTOS. [less ▲]

Detailed reference viewed: 42 (17 ULg)
Full Text
Peer Reviewed
See detailA LOTOS Data Facility Compiler (DAFY)
Lallemand, Eric; Leduc, Guy ULg

in Parther, Ken; Rose, Gordon (Eds.) Formal Description Techniques IV (1991, November)

If we take a look at existing LOTOS specifications, we notice that the description of the needed data types is very often huge. This causes the lack of concision of most descriptions of complex systems ... [more ▼]

If we take a look at existing LOTOS specifications, we notice that the description of the needed data types is very often huge. This causes the lack of concision of most descriptions of complex systems. We propose to tackle this problem in two steps. First, we define extensions to the LOTOS language allowing short definitions of most of the data types used in practical LOTOS specifications. Second, we propose a tool called `'DAFY'' (Data Facility Compiler) which is able to translate these extensions into standard LOTOS. [less ▲]

Detailed reference viewed: 14 (0 ULg)
Full Text
Peer Reviewed
See detailEquivalence associée à la relation de conformité "conf" et simplification du testeur canonique en LOTOS
Leduc, Guy ULg

in Rafiq, Omar (Ed.) CFIP'91 Ingénierie des Protocoles (1991, September)

Detailed reference viewed: 14 (0 ULg)
Full Text
Peer Reviewed
See detailConformance relation, associated equivalence, and minimum canonical tester in LOTOS
Leduc, Guy ULg

in Jonsson, B.; Parrow, J.; Pehrson, B. (Eds.) Protocol Specification, Testing, and Verification, XI (1991, June)

We first study the conf relation proposed by E. Brinksma and G. Scollo to formalise testing conformance. It is well-known from their work that, in order to test whether an implementation of a ... [more ▼]

We first study the conf relation proposed by E. Brinksma and G. Scollo to formalise testing conformance. It is well-known from their work that, in order to test whether an implementation of a specification S (i.e. I conf S), it suffices to build, from S, a canonical tester T(S) such that, when T(S) is synchronised with an implementation I, it always reaches a correct final state if, and only if, I conf S. For instance, if I is not a valid implementation of S, the canonical tester T(S) may deadlock with I before reaching a correct final state. We put into evidence the role of the equivalence relation, conf-eq, associated naturally with conf. An important result states that if S1 conf S2, their canonical testers T1 and T2 must also satisfy T1 conf-eq T2, and reversely. Therefore, the best approach is to define the canonical tester modulo conf-eq, whereas it is currently defined modulo the testing equivalence te. Taking into account that conf-eq is weaker than te, we were able to propose a minimum canonical tester which is simpler than T(S): unlike T(S), it may have fewer traces than the specification S. The term minimum means that no trace from this tester can be deleted without losing the exhaustive test property or, stated otherwise, without taking the risk of accepting an invalid implementation (in the conf sense). [less ▲]

Detailed reference viewed: 20 (1 ULg)
Full Text
See detailRelations d'implémentation et transformations autorisées d'une spécification LOTOS
Leduc, Guy ULg

in Réseaux et Informatique Répartie (1991), 1

Detailed reference viewed: 9 (1 ULg)
See detailLes applications informatiques des années 90 et leurs implications sur les réseaux de communication
Leduc, Guy ULg

in Bulletin Scientifique de l'Association des Ingénieurs Electriciens sortis de l'Institut Electrotechnique Montefiore (1991), 2

Detailed reference viewed: 17 (2 ULg)
Peer Reviewed
See detailA Framework for the Taxonomy of Synthesis and Analysis Activities in Distributed System Design
Dubuis, Eric; Gotzhein; Hansson, Hans et al

in Speth, R. (Ed.) Research into Networks and Distributed Applications (1988, April)

Detailed reference viewed: 20 (0 ULg)
Peer Reviewed
See detailArchitectural and Behavioural Modelling in Computer Communication
Blyth, David; Dubuis, Eric; Hansson, Hans et al

in Barton, M.; Dagless, E.; Reijns, G. (Eds.) Distributed Processing (1987, October)

Detailed reference viewed: 19 (3 ULg)
Peer Reviewed
See detailThe Intertwining of Data Types and Processes in LOTOS
Leduc, Guy ULg

in Rudin, Harry; West, Colin (Eds.) Protocol Specification, Testing and Verification, VII (1987, May)

Detailed reference viewed: 8 (1 ULg)
See detailLOTOS, un outil utile ou un autre langage académique ?
Leduc, Guy ULg

in Danthine, André (Ed.) Les réseaux de communication - nouveaux outils et tendances actuelles (1987, January)

Detailed reference viewed: 34 (2 ULg)
Peer Reviewed
See detailAssessing the Service Provided by a Connection-less Protocol
Leduc, Guy ULg

in Diaz, Michel (Ed.) Protocol Specification, Testing and Verification (1985, June)

Detailed reference viewed: 8 (2 ULg)