This page gathers information about tools and languages for LOTOS, E-LOTOS, and LOTOS NT. Its contents are divided into the following sections:
What is CADP?
CADP is a software package
offering a wide range of functionalities for the construction and analysis of
What is LNT?
LNT (a shorthand for "LOTOS New Technology") is a modern formal specification language that has been designed and implemented in the CADP toolbox since 2005. LNT is intended to be concise, expressive, easily readable, and user-friendly. LNT combines traits from process calculi, functional languages, and imperative languages. LNT should not be confused with earlier languages E-LOTOS and LOTOS NT (see below).
LNT is intensively used for specifying and verifying concurrent systems using CADP, in which LNT is progressively replacing LOTOS as the preferred high-level modelling language. At present, LNT is implemented by translation to LOTOS.
What is LOTOS?
To explain LOTOS in a nutshell, we could not do better than quoting the excellent definition of LOTOS given by the Research Unit in Networking of the University of Liège:
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 (ISO 8807:1989).
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.
Using Formal Description Techniques - An Introduction to ESTELLE, LOTOS, and SDL
Kenneth J. Turner
John Wiley, 1993, 431 pages
LOTOS and Petri-Net Based Verification of Systems and Circuits
Department of Computer Science, The Technion, Haifa, Israel
Engenharia de Protocolos com LOTOS/ISO
Bernardo Gonçalves Riso, Cristiano Maciel, Ivanise Volpato de Souza, Leila Lisiane Rossi, Mirela Sechi Moretti Annoni Notare, and Neilor Avelino Tonin
UFSC, 2004, 215 pages
Concurrency Theory, Calculi and Automata for Modelling Untimed and Timed Concurrent Systems
Howard Bowman and Rodolfo S. Gomez
Springer, 2006, 459 pages
Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS
Michael Yoeli and Rakefet Kol
Wiley, 2008, 231 pages
Introduction to the ISO Specification Language LOTOS
Tommaso Bolognesi and Ed Brinksma
Computer Networks and ISDN Systems, vol. 14(1), pp. 25-59
January 1987, 66 pages
The Formal Specification Language LOTOS: A Course for Users
Kenneth J. Turner
Technical Report, Dept of Computer Science and Mathematics, University of Stirling, Scotland
August 1989, 87 pages
An Introduction to LOTOS: Learning by Examples
L. Logrippo, M. Faci, M. Haj-Hussein
Computer Networks and ISDN Systems, vol. 23(5), pp. 325-342
Errata in 25(1) 99-100
1999, 34 pages
A Tutorial on ADT Semantics for LOTOS Users - Part I: Fundamental Concepts
José A. Mañas
Technical Report, Dpt. Ingenieria Telematica, E.T.S.I. Telecommunicion, Madrid, Spain
November 1988, 27 pages
A Tutorial on ADT Semantics for LOTOS Users - Part II: Operation on Types
José A. Mañas
Technical Report, Dpt. Ingenieria Telematica, E.T.S.I. Telecommunicion, Madrid,
November 1988, 27 pages
An Exercise in Formalizing the Description of a Concurrent System
D. W. Bustard, M. T. Norris, R. A. Orr, and A. C. Winstanley
Software Practice and Experience, vol. 22(12), pp. 1069-1098
December 1992, 30 pages
Introduction to Algebraic Specifications Based on the Language ACT ONE
Jan de Meer, Rudolf Roth and Son Vuong
Computer Networks and ISDN Systems, vol. 23(5), pp. 363-392 (1992)
Formal description technique (FDT) languages for protocols
Also at: http://dx.doi.org/10.1016/0169-7552(92)90013-G
LOTOS and the Formal Specification of Communication Standards: An Example
Alastair J. Tocher
In P. N. Scharbach, editor, Formal Methods: Theory and Practice. CRC Press, Inc., 1989.
An Example of LOTOS Specification: the Matrix Switch Problem
Hubert Garavel and Carlos Rodríguez
June 1990, 12 pages.
Présentation du langage LOTOS
November 1989, 38 pages, in French
Introduction au langage LOTOS
1990, 14 pages, in French
Software engineering in computer networks
Université de Liège, Belgium
An Introduction to LOTOS
Arturo Azcorra Salona, Juan Quemada Vives, Santiago Pavon Gomez
Dpto. Ingenieria de Sistemas Telematicos, Universidad Politecnica de Madrid
1993, 112 pages
A LOTOS Vade Mecum
Kenneth J. Turner, University of Stirling
1996, 2 pages
The two following languages are not supported by CADP. See the article entitled "From LOTOS to LNT
" for a retrospective discussion of E-LOTOS and LOTOS NT.
What is E-LOTOS?
E-LOTOS is an ISO/IEC international standard. It is not directly implemented in CADP. However, the best traits of E-LOTOS have been retained for LNT. These are a few links regarding E-LOTOS:
What is LOTOS NT?
LOTOS NT (where "NT" stands for "New Technology") is a simplified variant of E-LOTOS. Until 2014, "LOTOS NT" and "LNT" have been used as synonyms, but a clear distinction is now made between both languages. From now on, LOTOS NT is exclusively used when referring to the language accepted as input and translated into C code by the TRAIAN compiler.
TRAIAN only supports the data type part of LOTOS NT and is primarily used to build compilers and translators.
TRAIAN is also developed at INRIA Grenoble, but not part of the CADP toolbox.
These are a few links regarding LOTOS NT:
Version 1.80 last updated on 2017/10/23 18:16:08
Back to the CADP Home Page