Language Of Temporal Ordering Specification

Language Of Temporal Ordering Specification (LOTOS) is a formal specification language based on temporal ordering of events. LOTOS is used for protocol specification in ISO OSI standards.

LOTOS is an algebraic language that consists of two parts: a part for the description of data and operations, based on abstract data types, and a part for the description of concurrent processes, based on process calculus.

Work on the standard was completed in 1988, and it was published as ISO 8807 in 1989. Between 1993 and 2001, an ISO committee worked to define a revised version of the LOTOS standard, which was published in 2001 as E-LOTOS.

See also


  • ISO/IEC international standard 8807:1989. Information Processing Systems - Open Systems Interconnection - LOTOS: A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. Geneva, September 1989.
  • The Formal Description Technique LOTOS, P.H.J. van Eijk et al., editors, North-Holland, 1989.
  • LOTOSphere: Software Development with LOTOS, Tommaso Bolognesi, Jeroen van de Lagemaat, and Chris Vissers, editors, Kluwer Academic Publishers, 1995.
  • Hubert Garavel, Frédéric Lang, and Wendelin Serwe, From LOTOS to LNT. In Joost-Pieter Katoen, Rom Langerak, and Arend Rensink, editors, ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, vol. 10500 of Lecture Notes in Computer Science, pages 3-26, Springer International Publishing, October 2017, doi 10.1007/978-3-319-68270-9_1.

External links

This article is based on material taken from the Free On-line Dictionary of Computing prior to 1 November 2008 and incorporated under the "relicensing" terms of the GFDL, version 1.3 or later.

Algebraic data type

In computer programming, especially functional programming and type theory, an algebraic data type is a kind of composite type, i.e., a type formed by combining other types.

Two common classes of algebraic types are product types (i.e., tuples and records) and sum types (i.e., tagged or disjoint unions or variant types).The values of a product type typically contain several values, called fields. All values of that type have the same combination of field types. The set of all possible values of a product type is the set-theoretic product, i.e., the Cartesian product, of the sets of all possible values of its field types.

The values of a sum type are typically grouped into several classes, called variants. A value of a variant type is usually created with a quasi-functional entity called a constructor. Each variant has its own constructor, which takes a specified number of arguments with specified types. The set of all possible values of a sum type is the set-theoretic sum, i.e., the disjoint union, of the sets of all possible values of its variants. Enumerated types are a special case of sum types in which the constructors take no arguments, as exactly one value is defined for each constructor.

Values of algebraic types are analyzed with pattern matching, which identifies a value by its constructor or field names and extracts the data it contains.

Algebraic data types were introduced in Hope, a small functional programming language developed in the 1970s at the University of Edinburgh.

Calculus of communicating systems

The calculus of communicating systems (CCS) is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel composition, choice between actions and scope restriction. CCS is useful for evaluating the qualitative correctness of properties of a system such as deadlock or livelock.According to Milner, "There is nothing canonical about the choice of the basic combinators, even though they were chosen with great attention to economy. What characterises our calculus is not the exact choice of combinators, but rather the choice of interpretation and of mathematical framework".

The expressions of the language are interpreted as a labelled transition system. Between these models, bisimilarity is used as a semantic equivalence.

Communicating sequential processes

In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi, based on message passing via channels. CSP was highly influential in the design of the occam programming language, and also influenced the design of programming languages such as Limbo, RaftLib, Go, Crystal, and Clojure's core.async.

CSP was first described in a 1978 paper by Tony Hoare, but has since evolved substantially. CSP has been practically applied in industry as a tool for specifying and verifying the concurrent aspects of a variety of different systems, such as the T9000 Transputer, as well as a secure ecommerce system. The theory of CSP itself is also still the subject of active research, including work to increase its range of practical applicability (e.g., increasing the scale of the systems that can be tractably analyzed).

Construction and Analysis of Distributed Processes

CADP (Construction and Analysis of Distributed Processes) is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team (formerly by the VASY team) at INRIA Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.

The purpose of the CADP toolkit is to facilitate the design of reliable systems by use of formal description techniques together with software tools for simulation, rapid application development, verification, and test generation.

CADP can be applied to any system that comprises asynchronous concurrency, i.e., any system whose behavior can be modeled as a set of parallel processes governed by interleaving semantics. Therefore, CADP can be used to design hardware architecture, distributed algorithms, telecommunications protocols, etc.

The enumerative verification (also known as explicit state verification) techniques implemented in CADP, though less general that theorem proving, enable an automatic, cost-efficient detection of design errors in complex systems.

CADP includes tools to support use of two approaches in formal methods, both of which are needed for reliable systems design:

Models provide mathematical representations for parallel programs and related verification problems. Examples of models are automata, networks of communicating automata, Petri nets, binary decision diagrams, boolean equation systems, etc. From a theoretical point of view, research on models seeks for general results, independent of any particular description language.

In practice, models are often too elementary to describe complex systems directly (this would be tedious and error-prone). A higher level formalism known as process algebra or process calculus is needed for this task, as well as compilers that translate high-level descriptions into models suitable for verification algorithms.


E-LOTOS (Enhanced LOTOS) is a formal specification language designed between 1993 and 1999, and standardized by ISO in 2001.E-LOTOS was initially intended to be as a revision of the LOTOS language standardized by ISO 8807 in 1989. But the revision turned out to be profound, leading to a new specification language.

The starting point for the revision of LOTOS was the PhD thesis of Ed Brinksma, who had been the Rapporteur at ISO of the LOTOS standard.

In 1993, the initial goals of the definition of E-LOTOS have been stated in this announcement.In 1997, when the language definition reached the maturity level of an ISO Committee Draft, the following announcement was posted, which describes the main features of E-LOTOS.

The following document recalls the milestones of E-LOTOS definition project.

E-LOTOS has inspired descendent languages, among which LOTOS NT and LNT.

List of model checking tools

This article lists model checking tools and gives a synthetic overview their functionalities.


Lotos may refer to:

Grupa Lotos, oil company

Lotos Kolej, railway company

LOTOS Goldbrillen GmbH, a German luxury eyewear company founded in 1872

Lotos (satellite), a Russian family of electronic intelligence satellites

Language Of Temporal Ordering Specification

The Lotos-Eaters, a poem by Alfred Tennyson

ISO standards by standard number

This page is based on a Wikipedia article written by authors (here).
Text is available under the CC BY-SA 3.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.