[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Tutorials for CADP, LNT, and LOTOS
This page is an entry point gathering information about CADP, and about languages such as LNT, LOTOS, and E-LOTOS. 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 is a high-level modelling language meant to replace LOTOS. LNT draws inspiration from earlier languages, among which Ada, CCS, CSP, Occam, LOTOS, and E-LOTOS.

Motivation

Semantic foundations
Software implementations

There exist two compilers for LNT: TRAIAN, an LNT→C translator, and LNT2LOTOS, an LNT→LOTOS translator. Initially, these two compilers have been developed independently at different times. Since 2020, they are being brought increasingly closer.

TRAIAN has been developed since 1996 and comprises 56,000+ non-blank lines of code (July 2024). At the moment, it generates C code only for LNT data-type and function definitions. TRAIAN has been used for compiler construction since 2002. For instance, many CADP translators (including LNT2LOTOS and TRAIAN itself) are mainly written in LNT (80% of the code) and built using TRAIAN.

LNT2LOTOS has been developed since 2005 and comprises 45,000+ non-blank lines of code (July 2024). It implements LNT by translation to LOTOS, so as to reuse the existing CADP tools for LOTOS. It is intensively used for the study of concurrent systems by means of simulation, test generation, and formal verification using model checking and/or equivalence checking.

Each new version of TRAIAN and LNT2LOTOS is carefully checked using several test suites, which gather 23,900+ LNT programs totalling 15,000,000+ non-blank lines of LNT code (July 2024).

Until 2014, "LOTOS NT" and "LNT" were used as synonyms. Between 2014 and 2024, a distinction was made between the LOTOS NT language implemented in TRAIAN and the LNT language implemented in LNT2LOTOS, so as to point out the differences between both languages. These differences have been gradually removed, to the point that, since October 2023, TRAIAN is being used as a compiler-front end for LNT and systematically invoked before LNT2LOTOS. From now on, occurrences of "LOTOS NT" are progressively be replaced with "LNT".

Reference definition

The definition of LNT is given in two manuals: one for TRAIAN, one for LNT2LOTOS. These manuals are regularly updated and are ultimately set to merge, as the two compilers are progressively converging.

Slide shows

Other presentations can be found on our Education and Training page.

Complete examples in LNT

Compiler construction using 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
LOTOS as implemented in the CADP toolbox
Books
Articles and reports
Comparative surveys
Slide shows
Language leaflets
Defect report
Related Web pages

4. Miscellaneous: 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:

Version 1.114 last updated on 2024/12/10 11:23:32

Back to the CADP Home Page