References of "Léonard, Luc"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailModel-based verification of a security protocol for conditional access to services
Leduc, Guy ULg; Bonaventure, Olivier; Koerner, Eckhart et al

in Formal Methods In System Design (1999), 14(2), 171-191

We use the formal language LOTOS to specify and verify the robustness of the Equicrypt protocol under design in the European OKAPI project for conditional access to multimedia services. We state some ... [more ▼]

We use the formal language LOTOS to specify and verify the robustness of the Equicrypt protocol under design in the European OKAPI project for conditional access to multimedia services. We state some desired security properties and formalize them. We describe a generic intruder process and its modelling, and show that some properties are falsified in the presence of this intruder. The diagnostic sequences can be used almost directly to exhibit the scenarios of possible attacks on the protocol. Finally, we propose an improvement of the protocol which satisfies our properties. [less ▲]

Detailed reference viewed: 8 (0 ULg)
Full Text
Peer Reviewed
See detailA formal definition of time in LOTOS
Léonard, Luc; Leduc, Guy ULg

in Formal Aspects of Computing (1998), 10(3), 248-266

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

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

Detailed reference viewed: 21 (8 ULg)
Full Text
Peer Reviewed
See detailA formal definition of time in LOTOS (Full version)
Léonard, Luc; Leduc, Guy ULg

in Formal Aspects of Computing (1998), 10E

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

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

Detailed reference viewed: 16 (3 ULg)
Full Text
See detailQoS specification of ODP binding objects
Février, Arnaud; Najm, Elie; Leduc, Guy ULg et al

in Telektronikk (1997), 93(1), 42-49

We present a QoS oriented notation suitable for the ODP framework. In particular, we focus on a computational view of objects: we consider systems described as configurations of interacting objects and we ... [more ▼]

We present a QoS oriented notation suitable for the ODP framework. In particular, we focus on a computational view of objects: we consider systems described as configurations of interacting objects and we deal with two types of communications: message passing and flows. In message passing, signals (from one object to another) are conveyed through the (implicit) underlying infrastructure. This form of interaction is suitable for client/server applications where no strong real time or ordering constraints are needed from the communication infrastructure. In contract, in a flow type of communication, signals are conveyed through third party (binding) objects that may be explicitly called for in order to ensure specific QoS requirements needed by specific applications. A building blocks approach for the formal specification of binding objects in the ODP computational model is presented. The formal notation that is used is based on LOTOS extended with two features - real time and gate passing. These features are among the extensions that are currently studied in the ISO standardisation Formal Description Techniques group. We apply our building blocks approach to the specification of a multicast, multimedia binding object. [less ▲]

Detailed reference viewed: 12 (3 ULg)
Full Text
Peer Reviewed
See detailAn introduction to ET-LOTOS for the description of time-sensitive systems
Léonard, Luc; Leduc, Guy ULg

in Computer Networks & ISDN Systems (1997), 29(3), 271-292

Enhanced Timed-LOTOS, called ET-LOTOS, is an extension of LOTOS allowing the modelling of time-sensitive systems (i.e. systems whose behaviour is influenced by the passing of time). It is the basis of the ... [more ▼]

Enhanced Timed-LOTOS, called ET-LOTOS, is an extension of LOTOS allowing the modelling of time-sensitive systems (i.e. systems whose behaviour is influenced by the passing of time). It is the basis of the timed extension of LOTOS currently developed by ISO (1995). The purpose of this paper is to present ET-LOTOS in a tutorial style and show its applicability. The detailed study of the formal semantics is addressed in another paper. A collection of small but realistic, examples illustrates a wide variety of time-sensitive protocol mechanisms. These examples are used to introduce and justify the extensions of our language. Finally, the basics of the formal semantics are given and a comparison is made with other timed formalisms. [less ▲]

Detailed reference viewed: 12 (1 ULg)
Full Text
Peer Reviewed
See detailSpecification and verification of a TTP protocol for the conditional access to services
Leduc, Guy ULg; Bonaventure, Olivier; Koerner, Eckhart et al

in Formal Methods and their Applications: Telecommunications, VLSI and Real-Time Computerized Control Systems (1996, October)

We use the formal language LOTOS to specify the Equicrypt protocol and verify its robustness to attacks by an intruder. We use the model-based CADP verification tools from the Eucalyptus toolbox to ... [more ▼]

We use the formal language LOTOS to specify the Equicrypt protocol and verify its robustness to attacks by an intruder. We use the model-based CADP verification tools from the Eucalyptus toolbox to discover some successful attacks against this protocol. [less ▲]

Detailed reference viewed: 57 (3 ULg)
Full Text
Peer Reviewed
See detailCompositional Specification of ODP Binding Objects
Février, Arnaud; Najm, Elie; Leduc, Guy ULg et al

in Information Network and Data Communication (1996, June)

A building blocks approach for the formal specification of binding objects in the ODP Computational Model is presented. The formal notation that is used is based on LOTOS extended with two features - real ... [more ▼]

A building blocks approach for the formal specification of binding objects in the ODP Computational Model is presented. The formal notation that is used is based on LOTOS extended with two features - real time and gate passing. These features are among the extensions that are currently studied in the ISO standardisation Formal Description Techniques group. We apply our building blocks approach to the specification of a multicast, multimedia binding object. [less ▲]

Detailed reference viewed: 11 (0 ULg)
Full Text
See detailAn Extended LOTOS for the design of Real-Time Systems
Léonard, Luc; Leduc, Guy ULg

in Design and Analysis of Real Time Systems (1995, November)

We give a brief presentation of ET-LOTOS. ET-LOTOS extends with quantative time the formal description technique LOTOS. ET-LOTOS serves as basis for the time extension part of E-LOTOS, the new standard ... [more ▼]

We give a brief presentation of ET-LOTOS. ET-LOTOS extends with quantative time the formal description technique LOTOS. ET-LOTOS serves as basis for the time extension part of E-LOTOS, the new standard for LOTOS currently developed within ISO (ISO/IEC JTC1/SC21). [less ▲]

Detailed reference viewed: 12 (1 ULg)
See detailTime Extended LOTOS
Léonard, Luc; Leduc, Guy ULg

Report (1995)

Detailed reference viewed: 6 (1 ULg)
See detailA formal definition of time in LOTOS
Leduc, Guy ULg; Léonard, Luc

Report (1994)

Detailed reference viewed: 18 (3 ULg)
Full Text
See detailThe OSI95 Connection-Mode Transport Service
Baguette, Yves; Léonard, Luc; Leduc, Guy ULg et al

in The OSI95 Transport Service with Multimedia Support (1994)

We present the main features of the connection-mode service developed as a part of the entire OSI95 Enhanced Transport Service. This connection-mode service results from modifications and enhancements to ... [more ▼]

We present the main features of the connection-mode service developed as a part of the entire OSI95 Enhanced Transport Service. This connection-mode service results from modifications and enhancements to the standard ISO/IEC Connection-Mode Transport Service. Some of the enhancements are just mentioned in this paper for they are addressed in detail in companion papers. [less ▲]

Detailed reference viewed: 24 (1 ULg)
Full Text
See detailThe Tick-Tock Case Study for the Assessment of Timed FDT's
Léonard, Luc; Leduc, Guy ULg; Danthine, André ULg

in The OSI95 Transport Service with Multimedia Support (1994)

The initial purpose of this paper was to design a case study to assess LOTOS-T [MFV93] which is a temporal extension of LOTOS developed within the ESPRIT II OSI95 project. However, we think that it can be ... [more ▼]

The initial purpose of this paper was to design a case study to assess LOTOS-T [MFV93] which is a temporal extension of LOTOS developed within the ESPRIT II OSI95 project. However, we think that it can be useful for any proposed timed FDT. It consists of a protocol composed of two entities and an underlying service provider, whose behaviour is mainly based on various timing constraints such as time-out, isochronism, rate-control,... The selection of the mechanisms was guided by the two following characteristics: Realism: the selected mechanisms have been inspired by similar and existing protocol mechanisms or service facilities, even if we have tried to (over)simplify them in order to focus the case study on the timing constraints. Temporal modelling facilities: this means that the specificity and the variety of the timing constraints are intended to assess whether timed FDTs have enough power and flexibility to tackle a maximum number of aspects of timed behaviours. Of course, we do not pretend to have explored all possible timed behaviours which may exist in protocols. We have simply tried to cover a broad spectrum of them. [less ▲]

Detailed reference viewed: 20 (1 ULg)
Full Text
See detailBelgian-Spanish Proposal for a Time Extended LOTOS
Léonard, Luc; Leduc, Guy ULg; de Frutos, David et al

Report (1994)

Detailed reference viewed: 8 (2 ULg)
Full Text
Peer Reviewed
See detailAn Enhanced Version of Timed LOTOS and its Application to a Case study
Léonard, Luc; Leduc, Guy ULg

in Tenney, R. L.; Amer, P. D.; Uyar, M. U. (Eds.) FORMAL DESCRIPTION TECHNIQUES, VI (1993, October)

We propose here ET-LOTOS, a timed extension of LOTOS. It is an enhancement of Timed LOTOS that we presented at FORTE 92. We show how some simple modifications allow us to improve the expressiveness of our ... [more ▼]

We propose here ET-LOTOS, a timed extension of LOTOS. It is an enhancement of Timed LOTOS that we presented at FORTE 92. We show how some simple modifications allow us to improve the expressiveness of our former formalism. To assess ET-LOTOS, we apply it to the specification of a small case study. Finally, we show how the semantics of ET-LOTOS could be modified to easily define more powerful operators, if one ever had to. [less ▲]

Detailed reference viewed: 15 (4 ULg)
Full Text
See detailComment rendre LOTOS apte à spécifier des systèmes temps réel ?
Leduc, Guy ULg; Léonard, Luc

in Dssouli, Rachida; Bochmann, Gregor (Eds.) Ingénierie des Protocoles (1993, September)

We explain and justify by examples our proposed timed extension of LOTOS. The examples cover protocol functions and service facilities that are frequently encountered in practice or are inspired by ... [more ▼]

We explain and justify by examples our proposed timed extension of LOTOS. The examples cover protocol functions and service facilities that are frequently encountered in practice or are inspired by existing ones, such as timers, watchdogs, delays, isochronism, multimedia, rate control, ... The semantics of the language is presented after, and its properties discussed more formally. We think that the systematic application of formal temporal techniques to this kind of examples is unavoidable to convince of the pertinence of the design choices. The practical effectiveness of a formalism is as important as the associated mathematical properties. [less ▲]

Detailed reference viewed: 26 (1 ULg)
See detailThe OSI95 Enhanced Transport Services
Baguette; Léonard, Luc; Leduc, Guy ULg et al

Report (1993)

Detailed reference viewed: 19 (3 ULg)
Full Text
See detailQoS Enhancements and the new transport services
Danthine, André ULg; Bonaventure, Olivier; Baguette, Yves et al

in Onvural, R.; Nilsson, A. (Eds.) Local Area Network Interconnection (1993)

Detailed reference viewed: 12 (1 ULg)
Full Text
Peer Reviewed
See detailThe OSI 95 Connection-mode Transport Service-The Enhanced QoS
Danthine, André ULg; Baguette, Yves; Leduc, Guy ULg et al

in Danthine, André; Spaniol, Otto (Eds.) HIGH PERFORMANCE NETWORKING, IV (1992, December)

During the last ten years, tremendous changes have taken place in the communication environments. First, there has been a continuous increase in network performance that has led, for instance, to ... [more ▼]

During the last ten years, tremendous changes have taken place in the communication environments. First, there has been a continuous increase in network performance that has led, for instance, to increasingly high access data rates available in the lower layers. Furthermore, the changes in the offered network services have raised the issue of providing, at the transport level, services already provided at the subnetwork level, such as multicast or synchronous services for example. With the arrival of new applications, such as multimedia or client/server applications, a widening of the application requirements has also been observed. It is this evolving environment that has been at the origin of the ESPRIT II project OSI 95. An important task in the framework of this project is the definition of an enhanced Transport Service taking account of the aforementioned evolutions. The enhanced Transport Service specified for OSI 95 consists of several types of service. The paper presents the connection-mode Transport Service. We focus mainly on the following original features of our connection-mode service: a new semantics for QoS parameters and the associated negotiation and re-negotiation. [less ▲]

Detailed reference viewed: 78 (2 ULg)
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: 17 (2 ULg)
See detailOSI 95 Enhanced Transport Facilities and Functions
Baguette, Yves; Léonard, Luc; Leduc, Guy ULg et al

Report (1992)

Detailed reference viewed: 10 (2 ULg)