TRAIAN: A Compiler for LOTOS NT Specifications

TRAIAN 2.9 is available for download (Feb. 2018)

Version 1.75 - Date 2018/03/21 11:32:05

1. The E-LOTOS and LOTOS NT languages

Process algebras are often advocated as suitable formalisms for the specification of telecommunication protocols and distributed systems. However, despite their mathematical basis, despite standardization attempts (most notably the Formal Description Technique LOTOS), and despite an ever growing number of successful case-studies, process algebras have not yet reached a full acceptance in industry. On the other hand, description languages such as PROMELA or SDL are quite popular, although they lack a formal semantics, which might prohibit their use for safety-critical systems.

Our work was initiated in 1992 in the framework of the ISO/IEC Committee for the revision of the LOTOS standard. This standardization project aimed at the definition of E-LOTOS (or Enhanced LOTOS), a modern Formal Description Technique, which became an International Standard in 2001. See our E-LOTOS Web Page for detailed information about E-LOTOS.

At the same time E-LOTOS was being standardized, we started to study implementation issues for this language. Since the final version of E-LOTOS was not available yet, we based the research and development on a stable version of E-LOTOS called LOTOS NT (where "NT" stands for "New Technology").

Compared to algebraic languages (such as LOTOS, CCS, CSP, etc.) and non-algebraic ones (such as SDL and PROMELA), the LOTOS NT language aims at merging the "best of both worlds" by proposing a "second generation Formal Description Technique" that combines the strong theoretical foundations of process algebras with language features suitable for a wider industrial dissemination of formal methods.

For historical and technical reasons, there are two different implementations of LOTOS NT:

Notice that TRAIAN is not part of the CADP toolbox and must be installed separately if needed.

2. The TRAIAN compiler

TRAIAN is a prototype compiler for LOTOS NT developed by the VASY team (now the CONVECS team) at INRIA Rhône-Alpes. The name TRAIAN was chosen in honor of the Roman emperor (a successor of CAESAR...) who funded Romania.

TRAIAN is developed using SYNTAX and FNC-2, two compiler generation tools designed at INRIA Rocquencourt. It performs the following steps:

The following scientists have contributed to the development of TRAIAN:

Acknowledgements are due to Fabrice Baray, Estelle Dumas, Radu Mateescu, Gwen Salaün, Damien Thivolle, and Sai-Srikar Kasi for their valuable remarks about the TRAIAN compiler.

3. Release notes for TRAIAN

4. Download the latest version of TRAIAN

The current version of the TRAIAN compiler is version 2.9 released on February 28, 2018.

The following computer architectures and operating systems are currently supported by TRAIAN:

Additionally, the C code generated by TRAIAN, the include files, code libraries, and shell-scripts provided with TRAIAN also work on these computer architectures and operating systems:

TRAIAN is available for download from the VASY FTP server:

Please contact for any question or comment about TRAIAN.

5. Related publications

LOTOS NT User's Manual (Version 2.9)
Mihaela Sighireanu (with updates by Alban Catry, David Champelovier, Hubert Garavel, Frédéric Lang, Guillaume Schaeffer, Wendelin Serwe, and Jan Stöcker)
February 2018, 107 pages.

Etude et réalisation d'un compilateur E-LOTOS à l'aide du générateur de compilateurs SYNTAX/FNC-2
Bruno Vivien
December 1997, in French, 150 pages.

Towards a Second Generation of Formal Description Techniques - Rationale for the Design of E-LOTOS
Hubert Garavel and Mihaela Sighireanu.
May 1998, 28 pages.

Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire''): an Experiment with E-LOTOS
Mihaela Sighireanu and Radu Mateescu
June 1997, 37 pages.

Requirement Capture, Formal Description and Verification of an Invoicing System
Mihaela Sighireanu and Ken Turner
December 1998, 32 pages.

A Graphical Parallel Composition Operator for Process Algebras
Hubert Garavel and Mihaela Sighireanu
October 1999, 18 pages.

Compiler Construction using LOTOS NT
Hubert Garavel, Frédéric Lang, and Radu Mateescu
April 2002, 5 pages.

NTIF: A General Symbolic Model for Communicating Sequential Processes with Data
Hubert Garavel and Frédéric Lang
December 2002, 30 pages.

Hubert Garavel, Frédéric Lang, and Wendelin Serwe
October 2017, 29 pages.

You can find additional references from:

Back to the VASY Home Page