Research @ 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: 3.146.152.99...

RUN | Montefiore | ULg © 2000-2024.