LOTOS
ULg Research @ RUN RUN
LOTOS


Home

People

Research Topics

Projects

Publications

IFIP WG 6.1

Events and Conferences

CSS

How to Reach Us

Description

LOTOS is a Formal Description Technique (FDT) standardized by ISO for the design of distributed systems, and in particular for OSI services and protocols. Experts of the ISO FDT group developed LOTOS from 1981 to 1988; it has now the status of International Standard [IS 8807]. Unlike FDTs based on the state representation of a system, LOTOS describes a system by defining the temporal relations between externally observable events at so-called event gates. LOTOS is composed of two parts : a process algebraic part based on Milner's Calculus of Communicating Systems (CCS) and on Hoare's Communicating Sequential Processes (CSP), and a data algebraic part based on the abstract data type language (ACT ONE). These two aspects of LOTOS are complementary and independent : the process algebra is used to model dynamic behaviours of systems, and ACT ONE is used to model data structures and value expressions.

LOTOS has been widely used for the specification of large data communication systems. It is mathematically well-defined and expressive: it allows the description of concurrency, nondeterminism, synchronous and asynchronous communications. It supports various levels of abstraction and provides several specification styles. Good tools (e.g. the EUCALYPTUS toolset) exist to support specification, verification and code generation. Finally, LOTOS is one of the few process algebras to have moved out of the theoretical community.

LOTOS is currently under revision in ISO under the ELOTOS (Enhancements to LOTOS) activity to improve the datatype language and add features such as a module system and quantitative time.

More about LOTOS and ELOTOS

Research activities on LOTOS at RUN

In the EUCALYPTUS project we developed a datatype preprocessor for LOTOS, called APERO.

In the ACTS/OKAPI project, we use the formal language LOTOS to specify the Equicrypt protocol and verify its robustness to attacks by an intruder. We have used the model-based CADP verification tools from the Eucalyptus toolbox to discover some successful attacks against this protocol.

In the E-LOTOS activity, our proposal for a time extended LOTOS, called ET-LOTOS,has been retained by ISO and constitutes the body of annex C of the Revised Working Draft on ELOTOS (ISO/IEC JTC1/SC21/WG7 N1053). Later, in collaboration with Alan Jeffrey, we have integrated this proposal into a core data and behaviour language for E-LOTOS, which is available as chapter 3 of the Revised Working Draft (V4) on E-LOTOS (ISO/IEC JTC1/SC21/WG7 N1173). This core language is first-order, monomorphic, strongly typed and allows subtyping. It supports concurrency, real-time, exception handling, pattern-matching and some imperative features.

In a Belgian-French Tournesol co-operation project with the E.N.S.T. (Ecole Nationale Supérieure des Télécommunications), we have specified an ODP multimedia multicast binding object.

We were involved as Belgian delegate in the European Action COST 247 "Verification and Validation Methods for Formal Descriptions".

We were involved in three ESPRIT projects where we developed the following LOTOS specifications:

In the ESPRIT/APHRODITE project dealing with distributed software developments over a local network, LOTOS has been applied for the formal description of the CHORUS distributed operating system which underlies the whole architecture.

In the ESPRIT/PANGLOSS project dealing with the design of a high performance gateway using a top down approach, LOTOS has been used to specify the internet protocol at several stages of design.

In the ESPRIT/OSI95 project, LOTOS has been used to design a new transport service.


Publications

* Multimedia in the E-LOTOS Process Algebra
G. Leduc
Keywords : binding object, E-LOTOS, multicast, multimedia, ODP
Read the abstract
Download the PostScript document
Chapter 16 of "Formal Methods For Distributed Processing - A Survey of Objet Oriented Approaches", Cambridge University Press, 2001, pp. 357-372
* Introduction à E-LOTOS
G. Leduc, A. Jeffrey and M. Sighireanu
Keywords : E-LOTOS, formal method, timed process algebra, tutorial
Download the PostScript document
Chapitre 6 de "Ingénierie des protocoles et qualité de service", Hermès Science, France, 2001, pp. 213-252
* Spécification formelle pour la qualité de service dans l'Internet
G. Leduc and L. Kuty
Keywords : E-LOTOS, formal method, policer, RED, scheduler, shaper, timed process algebra, token bucket, WFQ
Mots-clés : contrôle de trafic, E-LOTOS, gestion des files d'attente, ordonnancement, qualité de service, régulation de trafic, services différenciés, spécification
Download the PDF document
Chapitre 3 de "Ingénierie des protocoles et qualité de service", Hermès Science, France, 2001, pp. 83-120
* Verification of Security Protocols using LOTOS - Method and Application
G. Leduc and F. Germeau
Keywords : LOTOS, model-checking, protocol verification, security protocol
Read the abstract
Download the PDF document
Computer Communications, special issue on Formal Description Techniques in Practice, vol. 23, nb. 12, Jul. 2000, pp. 1089-1103
(ISI IF 2000 = 0.341)
* Verification of two versions of the Challenge Handshake Authentication Protocol (CHAP)
G. Leduc
Keywords : model-checking, security protocols, verification
Read the abstract
Download the PostScript document
Annals of Telecommunications, vol. 55, nbs. 1-2, Jan.-Feb. 2000, pp. 18-30
(ISI IF 2000 = 0.292)
* Model-Based Verification of a Security Protocol for the Conditional Access to Services
G. Leduc, O. Bonaventure, E. Koerner, L. Léonard and C. Pecheur
Keywords : Equicrypt, LOTOS, model checking, security protocols
Read the abstract
Download the PostScript document
Formal Methods in System Design, vol. 14, nb. 2, March 1999, pp. 171-191
* A formal definition of time in LOTOS
L. Léonard and G. Leduc
Keywords : ET-LOTOS, LOTOS, negative premises, operational semantics, real time
Read the abstract
Download the PDF document
Formal Aspect of Computing, vol. 10 E, 1998, pp. 28-96
* A formal definition of time in LOTOS - Extended abstract
L. Léonard and G. Leduc
Keywords : ET-LOTOS, LOTOS, negative premises, operational semantics, real time
Read the abstract
Download the PDF document
Formal Aspects of Computing, vol. 10, nb. 3, 1998, pp. 248-266
* A Computer Aided Design of a Secure Registration Protocol
F. Germeau and G. Leduc
Keywords : authentication, formal verification, Guillou-Quisquater, LOTOS sprecification, registration protocol, security, trusted third party
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of Formal Description Techniques X / Protocol Specification, Testing and Verification XVII (FORTE/PSTV'97), Nov. 1997, Osaka, Japan, Chapman and Hall
* Applying LOTOS to the Design of TINA Applications
E. Koerner and L. Strick
Keywords : LOTOS, ODP viewpoints, TINA, verification, viewpoint compliance
Read the abstract
Proc. of the Second IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'97), Jul. 1997, Canterbury, UK, H. Bowman, J. Derrick (eds.), IFIP TC6 WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, pp. 455-466, Chapman and Hall
* Model-based Design and Verification of Security Protocols using LOTOS
F. Germeau and G. Leduc
Keywords : authentication, formal verification, LOTOS specification, registration protocol, security, trusted third party
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of the DIMACS Workshop on Design and Formal Verification of Security Protocols, 3-5 Sep. 1997, Rutgers University, New Jersey
* An introduction to ET-LOTOS for the description of time-sensitive systems
L. Léonard and G. Leduc
Keywords : ET-LOTOS, formal methods, LOTOS, specification, time
Read the abstract
Download the PDF document
Computer Networks and ISDN Systems, vol. 29, nb. 3, 1997, pp. 271-292
* QoS specification of ODP binding objects
A. Février, E. Najm, G. Leduc and L. Léonard
Read the abstract
Telektronnikk, vol. 93, nb. 1, Mar. 1997, pp. 42-49
* Specification and verification of a TTP protocol for the conditional access to services
G. Leduc, O. Bonaventure, E. Koerner, L. Léonard, C. Pecheur and D. Zanetti
Keywords : formal verification, LOTOS, model-checking, security protocol
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of the 12th J. Cartier Workshop on Formal Methods and their Applications: Telecommunications, VLSI and Real-Time Computerized Control Systems, Oct. 1996, Montreal, Canada
* Compositional Specification of ODP Binding Objects
A. Février, E. Najm, G. Leduc and L. Léonard
Keywords : binding object, LOTOS, MT-LOTOS, ODP
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of the 6th IFIP/ICCC Conference on Information Network and Data Communication (INDC'96), Jun. 1996, Trondheim, Norway
* An Extended LOTOS for the design of Real-Time Systems
L. Léonard and G. Leduc
Keywords : ET-LOTOS, LOTOS, process algebra, real-time
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of the Workshop on Design and Analysis of Real Time Systems (DARTS'95), Nov. 1995, Brussels, Belgium
* Failure-based Congruences, Unfair Divergences and New Testing Theory
G. Leduc
Keywords : debugging, formal languages, testing
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of 14th Conf. on Protocol Specification, Testing, and Verification (PSTV), Jun. 1994, Vancouver, Canada, S. Vuong, S. Chanson (eds.), Protocol Specification, Testing and Verification, XIV, pp. 252-267, Chapman & Hall, London, 1995
* The LOTOS Specification of the Enhanced Transport Service
L. Léonard
Keywords : LOTOS, OSI95, specification, transport service
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
In "The OSI95 Transport Service with Multimedia Support", Springer, 1994, pp. 239-244
* A Method for Applying LOTOS at an Early Design Stage and Its Application to the ISO Transport Protocol
G. Leduc
Keywords : constraint-oriented style, formal specification, LOTOS, transport protocol
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
In "The OSI95 Transport Service with Multimedia Support", Springer, 1994, pp. 151-180
* An enhanced Version of Timed LOTOS and its Application to a Case Study
L. Léonard and G. Leduc
Keywords : formal definitions and theory, formal languages, language constructs and features, mathematical logic and formal languages, programming languages
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of the IFIP TC6/WG6.1 Sixth International Conference on Formal Description Techniques (FORTE '93), 26-29 Oct. 1993, Boston, Massachusetts, R. Tenney, P. Amer, M. Uyar (eds.), Formal Description Techniques VI, IFIP Transactions, C-22, pp. 483-498, Elsevier Science
* VLib: Infinite virtual libraries for LOTOS
C. Pecheur
Keywords : languages constructs and features, processors, programming languages
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of the IFIP TC6/WG6.1 Thirteenth International Symposium on Protocol Specification, Testing and Verification, 25-28 May 1993, Liège, Belgium, A. Danthine, G. Leduc, P. Wolper (eds.), Protocol Specification, Testing and Verification XIII, pp. 29-44, Elsevier Science
* Comment rendre LOTOS apte à spécifier des systèmes temps réel ?
G. Leduc and L. Léonard
Keywords : FDT, LOTOS, real time, specification language, timed-proces algebra
Read the abstract
Lisez le résumé
Download the PostScript document or the compressed PostScript (gzip) document
Actes de CFIP'93, Sep. 1993, Montréal, Canada, R. Dssouli, G. Bochmann (eds.), Ingénierie des Protocoles, pp. 407-425, Hermès Paris
* A timed LOTOS supporting a dense time domain and including new timed operators
G. Leduc and L. Léonard
Keywords : formal definitions and theory, formal languages, language constructs and features, mathematical logic and formal languages, programming languages
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of FORTE'92, 13-16 Oct. 1992, Perros-Guirec, France, M. Diaz, R. Groz (eds.), Formal Description Techniques V, IFIP Transactions, C-10, pp. 87-102, Elsevier Science
* A framework based on implementation relations for implementing LOTOS specifications
G. Leduc
Keywords : abstraction, FDT, implementation, implementation process, implementation relation, LOTOS, process algebra, refinement, specification, transformation conformance
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Computer Networks and ISDN Systems, nb. 25, 1992, pp. 23-41
* An upward compatible timed extension to LOTOS
G. Leduc
Keywords : FDT, LOTOS, real time, specification language, timed-process algebra
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of FORTE'91, Nov. 1991, Sydney, Australia, K. Parther, G. Rose (eds.), Formal Description Techniques IV, IFIP Transactions, C-2, pp. 217-232, Elsevier Science
* A LOTOS Data Facility Compiler (DAFY)
E. Lallemand and G. Leduc
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of FORTE'91, Nov. 1991, Sydney, Australia, K. Parther, G. Rose (eds.), Formal Description Techniques IV, IFIP Transactions, C-2, pp. 313-327, Elsevier Science
* Using LOTOS for Specifying the CHORUS Distributed Operating System Kernel
C. Pecheur
Keywords : CHORUS, distributed operating systems, formal description techniques, processing systems, specification languages LOTOS
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Computer Communications, vol. 15, Mar. 1992, pp. 93-102
* Equivalence associée à la relation de conformité "conf" et simplification du testeur canonique en LOTOS
G. Leduc
Actes de Colloque Francophone sur l'Ingénierie des Protocoles (CFIP'91), Sep. 1991, Pau, France, O. Rafiq (ed.), CFIP'91 Ingénierie des Protocoles, pp. 425-440, Hermès, Paris
* Relations d'implémentation et transformations autorisées d'une spécification LOTOS
G. Leduc
Réseaux et Informatique Répartie (Networking and Distributed Computing), vol. 1, 1991, pp. 59-86
* Conformance relation, associated equivalence, and minimum canonical tester in LOTOS
G. Leduc
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of PSTV XI, Jun. 1991, Stockholm, Sweden, B. Jonsson, J. Parrow, B. Pehrson (eds.), Protocol Specification, Testing, and Verification, XI, pp. 249-264, Elsevier Science
* The Intertwining of Data Types and Processes in LOTOS
G. Leduc
Proc. of 7th IFIP Int. Conf. on Protocol Specification, Testing and Verification (PSTV), May 1987, Zürich, Switzerland, H. Rudin and C. West (ed.), Protocol Specification, Testing and Verification, VII, pp. 123-136, Elsevier Science Publisher (North-Holland, 1987)
* LOTOS, un outil utile ou un autre langage académique ?
G. Leduc
Actes de 9è Journées Francophones sur l'Informatique (JFI), Jan. 1987, Liège, Belgique, A. Danthine (ed.), Les réseaux de communication - nouveaux outils et tendances actuelles, pp. 1-25, Dunod Informatique, 1987
* Assessing the Service Provided by a Connection-less Protocol
G. Leduc
Proc. of 5th IFIP Int. Workshop on Protocol Specification, Testing and Verification (PSTV), Jun. 1985, Moissac, France, M. Diaz (ed.), Protocol Specification, Testing and Verification, pp. 215-234, Elsevier Science Publishers (North-Holland), 1986

[ Home | People | Research Topics | Projects | Publications | IFIP WG 6.1 | Events and Conferences | CSS | How to Reach Us ]

Editor: - G. Leduc -
Webmaster: - C. Soldani -
Still running IPv4 at: 54.161.91.76... RUN | Montefiore | ULg
© 2000-2015.