Tutorials for CADP, LNT, and LOTOS
This page gathers information about tools and languages for LOTOS, E-LOTOS, and LOTOS NT. Its contents are divided into the following sections:
1. Tutorials for CADP

What is CADP?

CADP is a software package offering a wide range of functionalities for the construction and analysis of distributed processes.

Articles and reports

Videos
Related Web pages

2. Tutorials for LNT

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.

These are references regarding LNT:


3. Tutorials for 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.


Reference definition
Books
Articles and reports
Comparative surveys
Slide shows
Language leaflets
Defect report
Related Web pages

4. Miscellaneous: E-LOTOS and LOTOS NT


The two following languages are not supported by CADP.

Material about E-LOTOS

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 some links regarding E-LOTOS:

Material about LOTOS NT

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 some links regarding LOTOS NT:


Version 1.48 last updated on 2014/07/19 10:48:52

Back to the CADP Home Page