Hubert Garavel
email: hubert.garavel@inria.fr

Frédéric Lang
email: frederic.lang@inria.fr

Wendelin Serwe
email: wendelin.serwe@inria.fr

From LOTOS to LNT

Keywords: abstract data type, algebraic specification, concurrency theory, E-LOTOS, formal description technique, formal method, formal specification, LOTOS, LNT, process algebra, process calculus, specification language

We revisit the early publications of Ed Brinksma devoted, on the one hand, to the definition of the formal description technique LOTOS (ISO International Standard 8807:1989) for specifying communication protocols and distributed systems, and, on the other hand, to two proposals (Extended LOTOS and Modular LOTOS) for making LOTOS a simpler and more expressive language. We examine how this scientific agenda has been dealt with during the last decades. We review the successive enhancements of LOTOS that led to the definition of three languages: E-LOTOS (ISO International Standard 15437:2001), then LOTOS NT, and finally LNT. We present the software implementations (compilers and translators) developed for these new languages and report about their use in various application domains.

Introduction

The present article was written in honor of Ed Brinksma and included in a collective Festschrift book offered to him at the occasion of his 60th birthday.

The first part of Ed Brinksma's research career has been devoted to the design of formal methods for the specification of communication protocols and distributed systems, the LOTOS language being the common theme and vital lead for the scientific contributions. This first part approximately extends over twelve years, between 1984 (as dated by the conference article [START_REF] Brinksma | A Specification of the OSI Transport Service in LOTOS[END_REF]) and 1995 (as dated by the book chapter [START_REF] Brinksma | Enhancements of LOTOS[END_REF]). It was directly succeeded, with some chronological overlap, by a second part centered on conformance testing for protocols (with a first paper [START_REF] Brinksma | A Framework for Test Selection[END_REF] published in 1991) and a third part centered on real time and performance evaluation (with early papers, e.g., [START_REF] Brinksma | A Stochastic Causality-Based Process Algebra[END_REF] published in 1995).

In the present article, we focus on this first part, in which we distinguish two different threads of work: (i) the definition of the LOTOS language, which culminated with its adoption by ISO (International Standard 8807:1989) and (ii) the elaboration of two proposals for enhancing LOTOS, by introducing valuable features not present in the standard, either because they were not ready on time when it was adopted or because they did not reach international consensus.

The present article is organized as follows. Section 2 recalls the contributions of Ed Brinksma to the definition of LOTOS and gives a brief account of the impact of this language in academia and industry. The two next sections review two early languages proposed by Ed Brinksma for enhancing LOTOS, namely Extended LOTOS (Sect. 3) and Modular LOTOS (Sect. 4). The three next sections present three more recent languages that, between 1993 and now, have been proposed to supersede LOTOS, namely E-LOTOS (Sect. 5), LOTOS NT (Sect. 6), and LNT (Sect. 7), with some discussion about the actual impact of these languages. Finally, Section 8 gives a few concluding remarks.

LOTOS

Among all publications of Ed Brinksma related to the definition of LOTOS, we highlight three key contributions, each of a different nature and scope:

• Obviously, the ISO Draft International Standard defining LOTOS [START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF] occupies a place of choice. Even if earlier drafts of LOTOS had circulated before (e.g., Ed Brinksma's first tutorial on LOTOS [START_REF] Brinksma | A Tutorial on LOTOS[END_REF] given in 1985) and even if experiments with LOTOS had already been done at some universities (e.g., the model-checking verification of protocols in 1986 [START_REF] Garavel | Vérification de programmes LOTOS à l'aide du système QUASAR[END_REF][START_REF] Garavel | Utilisation du système CESAR pour la vérification de protocoles spécifiés en LOTOS[END_REF]), this Draft International Standard published in 1987 was the first complete, coherent definition of LOTOS made available to the international community. Two years after, this document reached its final status by being approved as the ISO International Standard 8807:1989 [START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF].

The definition of LOTOS was a collective achievement done within an ISO committee (project 97.21.20.2) under the leadership of Ed Brinksma, who was the editor in charge of producing the standard. Tommaso Bolognesi, Günter Karjoth, Luigi Logrippo, Jan de Meer, Elie Najm, Juan Quemada, Pippo Scollo, Alaister Tocher, Jan Tretmans, and Chris Vissers participated, among others, in this committee.

The resulting LOTOS language was an audacious combination of the most recent innovations in formal methods at that time. To describe and manipulate data structures, the LOTOS committee selected abstract data types -more precisely, a dialect of the algebraic language ACT ONE [START_REF] Ehrig | An Algebraic Specification Language with Two Levels of Semantics[END_REF] [27] [START_REF] De Meer | Introduction to Algebraic Specifications Based on the Language ACT ONE[END_REF]. To describe the behaviour of concurrent processes, the committee retained the key ideas of process algebra, blending into a single language the best features of several calculi, namely CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF], TCSP [START_REF] Brookes | A Theory of Communicating Sequential Processes[END_REF], and Circal [START_REF] Milne | CIRCAL and the Representation of Communication, Concurrency, and Time[END_REF]. LOTOS also brought original ideas, such as its "disable" operator, which models nondeterministic disruption (e.g., crashes and failures), and its "enable" operator, which allows value-passing sequential continuation after the termination of a group of parallel processes.

The definition of LOTOS provided in the ISO standard was fully formal, much in line with the longstanding Dutch tradition of computer-language definitions. The syntax was given as a BNF grammar; the static semantics was specified as a set of mathematical constraints and functions defined by induction over syntactic constructs; the semantics of data types was expressed as a many-sorted term algebra obtained by quotienting the algebra generated by a derivation system; finally the behavioural semantics of processes was defined operationally using a set of structured operational semantics rules. This formal definition was followed by annexes providing informal explanations and complementary information.

• Jointly written with Tommaso Bolognesi, Ed Brinskma's tutorial on LO-TOS [START_REF] Bolognesi | Introduction to the ISO Specification Language LOTOS[END_REF] is also a highly cited publication. Written in a lively style and illustrated with a wealth of examples, this tutorial targets the end users of LOTOS. It is orthogonal and complementary to the (somewhat dry) ISO standard definition, primarily oriented towards language implementers and semanticists.

• Another insightful contribution is Ed Brinskma's 1989 paper on constraint-oriented specification [START_REF] Brinksma | Constraint-Oriented Specification in a Constructive Formal Description Technique[END_REF]. It is well-known that the decomposition of a computer system into concurrent/parallel tasks may take two forms: it is either physical if the decomposition closely reflects the actual distribution of tasks over processors, or logical otherwise, if the decomposition is rather intended to provide the system with a modular structure that does not necessarily correspond to its actual topology. Ed Brinksma develops the latter approach in the framework of the LOTOS multiway rendezvous, which enables two or more processes to synchronize, negotiate, and exchange data values during one atomic event. The paper formulates the fundamental intuition of parallel composition as conjunction, meaning that the multiway rendezvous achieves the logical conjunction of all the individual constraints expressed by a set of processes running concurrently. This idea enables a certain degree of "declarative" programming (namely, constraint solving) to be introduced in the framework of a fundamentally "operational" (i.e., constructive, imperative) language such as LOTOS. The usefulness of the approach is demonstrated on realistic examples of communication protocols [START_REF] Brinksma | Constraint-Oriented Specification in a Constructive Formal Description Technique[END_REF], but it is also relevant to other application domains, e.g., hardware circuits ( [START_REF] Garavel | On Combining Functional Verification and Performance Evaluation using CADP[END_REF] shows how the complex arbitration protocol of the SCSI-2 bus can be concisely modelled using an eight-party LOTOS rendezvous) or robotics ([48] illustrates how a software controller for an entire manufacturing plant can be obtained as the parallel composition of many simple controllers, one for each device or degree of freedom of a device in the plant).

Retrospectively, the international effort invested in LOTOS was successful in several respects:

• Although LOTOS is a committee-designed language based on two very different concepts (algebraic data types and process calculi), it achieves a suitable compromise and a fair integration between its various elements. All its language constructs (perhaps with the exception of the choice and par operators on gate lists) derive from concrete needs and are useful in practice.

• LOTOS is clearly more abstract and higher level than the two other standardized languages it was competing with (namely, Estelle [START_REF] Iso/Iec | ESTELLE -A Formal Description Technique Based on an Extended State Transition Model[END_REF] and SDL [START_REF] Ccitt | Specification and Description Language[END_REF]), and proved that a specification language could be formal and executable at the same time.

• The design of LOTOS made it clear that process calculi were not only mathematical notations for studying concurrency theory, but that they could be turned into computer languages used to model real-life systems. LOTOS was indeed the first process calculus in which large specifications of complex systems (e.g., protocols and services of OSI and ISDN networks) were produced. Later, it was shown that the high abstraction level of LOTOS makes it also suitable to other application domains, e.g., multiprocessor architectures and asynchronous circuits.

• The LOTOS community put strong emphasis on software tools, often in the framework of European projects such as SEDOS, LOTOSphere, SPECS, EUCALYPTUS-1 and -2, etc. Today, most of these tools are no longer available, but the CADP toolbox1 [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] is still actively maintained. Also, many ideas present in early LOTOS tools would certainly benefit from modern developments in symbolic execution and verification technology.

On the negative side, one can point out two main shortcomings of LOTOS:

• Despite its status of international standard, LOTOS did not manage to unite the academic community working on process calculi. Not only the preexisting algebras/calculi ACP, CCS, and CSP remained, but new languages appeared, e.g., µCRL. This resulted in fragmented efforts and a lack of critical mass that became apparent in the mid-90s.

• LOTOS also failed to gain wide industrial acceptance, mostly due to its socalled "steep learning curve". Because it is an abstract, expressive, and flexible language based on concepts absent from mainstream languages, LOTOS is best used by high-level experts rather than average software programmers: this is unfortunately a fatal flaw as far as dissemination is concerned.

Extended LOTOS

As soon as the definition of LOTOS was frozen as an ISO standard, it appeared that the language was not fully satisfactory and that some of its features could be redesigned in a better way. Ed Brinksma's role as the editor of the LOTOS standard did not prevent him from suggesting enhancements to LOTOS.

His first contribution in this respect is his PhD thesis [START_REF] Brinksma | On the Design of Extended LOTOS -A Specification Language for Open Distributed Systems[END_REF], defended in 1988, which proposes a language named "Extended LOTOS" that significantly differs from LOTOS. Concerning data specifications, Extended LOTOS keeps the abstract data types of LOTOS, but adds better support for modules. Concerning behavioural specifications (namely, concurrent processes), Extended LOTOS brings deeper changes:

• It introduces a notion of action product inspired from SCCS [START_REF] Milner | Calculi for Synchrony and Asynchrony[END_REF], whereas LOTOS only has simple actions.

• Extended LOTOS attempts at unifying in one single operator both forms of sequential composition (action prefix and "enable") that exist in LO-TOS.

• Although Extended LOTOS has never been actually implemented, these ideas had the merit to point out the main shortcomings of LOTOS and made it clear that the language, despite its status of international standard, still deserved major enhancements.

Modular LOTOS

Published three years later, a deliverable (edited by Ed Brinksma) of the LO-TOSphere project [START_REF] Brinksma | Task 1.4 Deliverable on Language Enhancements, LOTO-Sphere[END_REF] adopts a point of view orthogonal to that of Extended LOTOS: leaving aside all ideas for improving the behaviour part of LOTOS, this deliverable focuses on enhancements to the data part of LOTOS, in which usability problems have been identified as most crucial, and proposes a new language called "Modular LOTOS", two synthetic presentations of which can also be found in [START_REF] Brinksma | Enhancements of LOTOS[END_REF] and [START_REF] Roth | Data Specifications in Modular LOTOS[END_REF]. Modular LOTOS suggests the following enhancements:

• Distinction between constructors and functions, whereas LOTOS made no difference between these two forms of operations;

• Introduction of partial functions, whereas LOTOS only allowed totally defined operations;

• Support for built-in types (e.g., natural numbers, integer numbers, strings) and generic data structures (e.g., lists, sets, arrays, etc.);

• Introduction of modules gathering data and/or behaviour definitions, namely, types, constructors, functions, and processes;

• Introduction of module interfaces (called descriptions) that can be used to hide certain definitions contained in modules;

• Introduction of renaming to avoid name clashes between different modules;

• Support for generic modules parameterized by descriptions.

To our knowledge, Modular LOTOS has never been implemented, although key ideas (namely, distinction between constructors and functions, partial functions, and splitting of large LOTOS specifications into multiple files) were already supported in the CAESAR.ADT compiler for LOTOS [START_REF] Garavel | Compilation of LOTOS Abstract Data Types[END_REF]. At this point, Ed Brinskma shifted his research interests to other topics, but the LOTOS reform movement he had initiated expanded rapidly.

E-LOTOS

Between 1993 and 2001, an ISO committee gathered under the lead of Juan Quemada to revise the LOTOS standard. Arnaud Février, Hubert Garavel, Alan Jeffrey, Guy Leduc, Luc Léonard, Luigi Logrippo, José Mañas, Elie Najm, Mihaela Sighireanu, and Jacques Sincennes participated in this committee as regular contributors, with the help of more than twenty occasional contributors [START_REF] Quemada | E-mail announcement available from[END_REF].

At the beginning, the proposed changes were modest, trying to repair rather than replace LOTOS; as time passed, it appeared that more radical enhancements were desirable. This work eventually resulted in a new language named E-LOTOS (for "Enhanced LOTOS") approved as ISO/IEC International Standard 15437:2001 [START_REF]ISO/IEC. Enhancements to LOTOS (E-LOTOS)[END_REF]. Tutorials on E-LOTOS can be found in [START_REF] Verdejo | Tutorial and Semantics[END_REF], [START_REF] Huecas | E-LOTOS: An Overview[END_REF][START_REF] Huecas | Process Calculi: E-LOTOS[END_REF] and [START_REF] Leduc | Introduction à E-LOTOS[END_REF]. Compared to LOTOS, E-LOTOS brings deep changes that aim at greater expressiveness and/or better user-friendliness:

• Concerning the data types, E-LOTOS goes far beyond the ideas suggested for Modular LOTOS. Rather than enhancing ACT-ONE, E-LOTOS removes it, replacing abstract data types with a functional languagean approach also explored in [START_REF] Berthomieu | Programming with Behaviors in an ML Framework -The Syntax and Semantics of LCS[END_REF], which proposes a concurrent language combining a process calculus (CCS) and a functional language (ML). E-LOTOS goes even further by giving its functional language an imperative flavour: in particular, E-LOTOS variables can be assigned and E-LOTOS functions can have output (i.e., call by result) parameters to return multiple results, which, in conventional functional languages, is usually done by returning tuple values.

• E-LOTOS data types can be records (with named or unnamed fields) or (possibly recursive) types defined by a list of constructors. E-LOTOS also provides predefined types (Booleans, naturals, integers, rationals, floatingpoint reals, characters, and strings) and abbreviations for declaring enumerated types, records, sets, and lists.

• Contrary to LOTOS, in which the data and behaviour parts are two entirely different sub-languages, E-LOTOS tries to unify functions and processes; functions can be seen as particular cases of processes that only do local calculations before terminating, do not perform any observable or invisible action, and do not let time elapse. Consequently, functions and processes share a number of common constructs, among which: variable assignments, if-then-else conditionals, case with pattern matching, while loops, for loops, etc.

• In both its data and behaviour parts, E-LOTOS introduces a unique sequential composition operator, which unifies the action-prefix and "enable" operators present in the behaviour part of LOTOS.

• E-LOTOS provides support for exception handling. In the data part of E-LOTOS, exceptions bring a convenient solution to the need for partial functions. In the behaviour part, exceptions allow some involved communication protocols to be described compositionally -see [START_REF] Garavel | On the Introduction of Exceptions in LOTOS[END_REF] for an advocacy paper on exceptions in process calculi.

• Gates (i.e., communication ports) are explicitly typed in E-LOTOS, whereas they are untyped in LOTOS -see [START_REF] Garavel | On the Introduction of Gate Typing in E-LOTOS[END_REF] for an introduction to gate typing, which leads to more readable specifications, detects communication mismatches at compile time rather than at run time, and provides a simple solution to the "structured events" issue in the constraint-oriented style.

• To express quantitative time aspects, the behaviour part of E-LOTOS allows to specify constraints on the duration of actions and/or the instant(s) at which they may occur. Such features are required to describe isochronous protocols and real-time systems precisely, and many timed extensions of LOTOS have been proposed, e.g., ET-LOTOS [START_REF] Léonard | An Introduction to ET-LOTOS for the Description of Time-Sensitive Systems[END_REF][START_REF] Léonard | A Formal Definition of Time in LOTOS[END_REF] and RT-LOTOS [START_REF] Courtiat | Outtaj. Experience with RT-LOTOS, a Temporal Extension of the LOTOS Formal Description Technique[END_REF].

• The behaviour part of E-LOTOS introduces a n-ary parallel operator [START_REF] Garavel | A Graphical Parallel Composition Operator for Process Algebras[END_REF] that generalizes the three binary parallel composition operators of LO-TOS. This new operator is easier to use, more readable, and enables mamong-n synchronization (in particular, the 2-among-n synchronization of CCS).

• The behaviour part of E-LOTOS also introduces new operators, such as rename (which allows to change the name of observable actions and exceptions, to merge or split gates, and to add or remove offers from actions) and suspend/resume (which generalizes the "disable" operator of LOTOS by allowing resumable interrupts to be modelled).

• Finally, E-LOTOS provides modules that may contain types, functions, and/or processes. Modules can be imported and exported; they have interfaces for information hiding and can be generic.

Due to its new features resulting from multiple, sometimes conflicting influences, and despite the unification between functions and processes, E-LOTOS is a complex language, with an impressive number of semantic rules. The E-LOTOS standard has 120 pages (+80 pages of annexes), while the LOTOS standard has only 70 pages (+70 pages of annexes). It is therefore unclear whether E-LOTOS brings a satisfactory answer to the "steep learning curve" issue with LOTOS.

This probably explains why E-LOTOS only had a marginal impact in practice. Very few case studies have been done using E-LOTOS; one can mention [START_REF] Sighireanu | Requirement Capture, Formal Description and Verification of an Invoicing System[END_REF][START_REF] Turner | ELOTOS: (Enhanced) Language Of Temporal Ordering Specification[END_REF] (which compares LOTOS and E-LOTOS on a common example), [START_REF] Lopes De Souza | Design of Distributed Multimedia Applications (DAMD)[END_REF], [START_REF] Clark | Use of E-LOTOS in Adding Formality to UML[END_REF], and [START_REF] Shankland | Time, E-LOTOS, and the FireWire[END_REF][START_REF] Shankland | A Case Study in Abstraction Using E-LOTOS and the FireWire[END_REF]. To our knowledge, E-LOTOS has never been implemented in software tools (except perhaps [START_REF] Lopes De Souza | Design of Distributed Multimedia Applications (DAMD)[END_REF] or [START_REF] Francisco | Simulator for E-LOTOS Specifications[END_REF]) nor taught in university classes.

In some sense, the shift from LOTOS to E-LOTOS is reminiscent of the shift from Algol 60 to Algol 68: a simple, elegant, yet limited language was replaced by a larger, more expressive, formally defined language, which, because of its growth in complexity, failed to build a sufficient momentum of interest among its potential users.

6 LOTOS NT

Design of LOTOS NT

In 1997, when it became manifest that E-LOTOS was getting too large and too complex, INRIA Grenoble started investigating a fallback solution. This led to the design of LOTOS NT (where "NT" stands for "New Technology"), a simplified dialect of E-LOTOS that could be feasibly implemented and provide an actual replacement solution for LOTOS.

It was decided to not introduce in LOTOS NT some questionable features that significantly contribute to the complexity of E-LOTOS, among which: type synonyms, anonymous tuples (i.e., the possibility, borrowed from ML, that any list of values put between parentheses creates a new value having a valid, yet undeclared tuple type), extensible records, type equality relation based on structure equivalence (rather than name equivalence), subtyping relation based on record subtyping, etc.

For the same reasons, two features present in E-LOTOS but absent from LO-TOS, the suspend-resume operator and the support for quantitative time, were not introduced in LOTOS NT, as it was felt that the potential applications of such features were already covered by competing formalisms such as timed automata [START_REF] Alur | A Theory of Timed Automata[END_REF] and were not worth the effort/impact ratio.

The formal definition of LOTOS NT (syntax, static semantics, and dynamic semantics) was given in [START_REF] Sighireanu | Contribution à la définition et à l'implémentation du langage "Extended LOTOS[END_REF]. Rationale for the design of LOTOS NT (and of E-LOTOS as well, since LOTOS NT influenced the latest evolutions of E-LOTOS) can be found in [START_REF] Garavel | Towards a Second Generation of Formal Description Techniques -Rationale for the Design of E-LOTOS[END_REF].

Implementation of LOTOS NT

To implement this language, a compiler named TRAIAN2 [START_REF] Sighireanu | LOTOS NT User's Manual (Version 2.8)[END_REF] has been developed at INRIA Grenoble since 1997. It is built using the SYNTAX [START_REF] Boullier | A New Error Repair and Recovery Scheme for Lexical and Syntactic Analysis[END_REF] and FNC-2 [START_REF] Jourdan | Application Development with the FNC-2 Attribute Grammar System[END_REF] compiler-generation tools designed at INRIA Rocquencourt. Unfortunately, FNC-2 ceased to be maintained in 1999, which prevented TRAIAN from being completed; as a consequence, TRAIAN only handles the data part of LOTOS NT (i.e., types and functions) but not the behaviour part (i.e., processes and channels).

As it is, TRAIAN performs lexical analysis, syntactic analysis, abstract syntax tree construction, static semantics analysis of LOTOS NT data specifications, and translates these into C programs, which can in turn be compiled and executed. TRAIAN has been regularly maintained and enhanced: ten releases have been issued since 1998, the latest version of TRAIAN (dated 2016) containing 55,500 lines of FNC-2 and C code.

Applications of LOTOS NT

Although TRAIAN only supports a fragment of LOTOS NT, it has useful applications in compiler construction. Our approach [START_REF] Garavel | Compiler Construction using LOTOS NT[END_REF] consists in using the SYNTAX compiler generator for the lexical and syntactic analyses, together with LOTOS NT for semantical aspects, in particular the definition, construction, and traversals of abstract trees. Some involved parts of the compiler can be written directly in C if necessary, but most of the compiler is usually written in LOTOS NT, which is then translated into C code by TRAIAN.

The combined use of SYNTAX, LOTOS NT, and TRAIAN proves to be satisfactory, as regards both the rapidity of development and the quality of resulting compilers. So far, twelve compilers have been developed at INRIA Grenoble using this approach:

AAL [START_REF] Mateescu | A Generic Framework for Model Checking Software Architectures[END_REF], AT-LANTIF [START_REF] Stoecker | Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format[END_REF], CHP2LOTOS [START_REF] Garavel | On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP[END_REF], CTRL2BLK [START_REF] Mateescu | Computation Tree Regular Logic for Genetic Regulatory Networks[END_REF], EVALUATOR 4.0 [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF], EXP.OPEN 2.0 [START_REF] Lang | EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods[END_REF], FSP2LOTOS [START_REF] Lang | Translating FSP into LOTOS and Networks of Automata[END_REF], GRL2LNT [START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF], LNT2LOTOS [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.7)[END_REF], NTIF [START_REF] Garavel | NTIF: A General Symbolic Model for Communicating Sequential Processes with Data[END_REF], PIC2LNT [START_REF] Mateescu | PIC2LNT: Model Transformation for Model Checking and Applied Pi-Calculus[END_REF], and SVL [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF][START_REF] Lang | Compositional Verification using SVL Scripts[END_REF][START_REF] Crouzen | Smart Reduction[END_REF].

LNT

Design of LNT

Because of the limitations of TRAIAN, LOTOS NT does not provide a replacement solution for LOTOS. The need for a better language based on process calculi remains [START_REF] Garavel | Défense et illustration des algèbres de processus[END_REF] [START_REF] Garavel | Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular[END_REF], even if all prior attempts have failed to provide a usable solution.

In 2005, a new opportunity was found to progress this agenda: the Bull company was interested in using the CADP toolbox to formally verify multiprocessor architectures, but was reluctant to use LOTOS as a modelling language, mostly due to the verbosity of the LOTOS data part. To ease the writing of large specifications by Bull, still using the existing CADP tools, INRIA Grenoble undertook the development of a translator to convert LOTOS NT data types and functions into LOTOS ones. This made it possible to produce specifications combining a data part written in LOTOS NT (more concise and less errorprone than LOTOS) and a behaviour part written in LOTOS. The translator converted such composite specifications into plain LOTOS ones, which then could be analyzed by the CADP tools.

A first version of this translator was delivered to Bull in July 2005. Since then, the translator has been constantly improved and extended to handle new LOTOS NT features. In 2007, support for the behaviour part of LOTOS NT was added; this progressively removed the need for composite specifications, as it became possible to write entire specifications in LOTOS NT, with no LOTOS code at all. Due to the rapid evolution of this translator, its input language gradually diverged from the original LOTOS NT implemented in TRAIAN, which remained quite stable in comparison. To avoid ambiguities, it was decided in 2014 to give this input language a new name ("LNT"), while reserving the name "LO-TOS NT" for the language accepted by TRAIAN -such a distinction was not made in papers published before Spring 2014, in which LOTOS NT and LNT were used as synonyms.

The current definition of LNT is given in [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.7)[END_REF]. In a nutshell, LNT combines, in a single language with an Ada-like syntax designed to favour readability, selected features borrowed from imperative languages, functional languages, and valuepassing process calculi:

• An LNT specification is a set of modules, each of which may import other modules and define types, functions, channels, and/or processes.

• A type is either predefined (namely, bool, nat, int, real, char, and string), defined by specifying the free constructors that generate its domain of values, or defined using the type combinators array, list, range, set, sorted list, sorted set, and where (the latter enabling predicate subtyping).

• A function is either predefined (namely, logical, arithmetical, and relational operations on predefined types), automatically generated for some user-defined type (such as free constructors, but also equality, order relations, field accessors and selectors, etc., which are generated if the user requests them), or have a handwritten definition provided by the user.

• A channel is a gate type that, following the ideas of [START_REF] Garavel | On the Introduction of Gate Typing in E-LOTOS[END_REF], specifies the types of values to be sent or received during interactions on a given gate. There exist two special channels: none, which expresses that no value can be sent or received (this is useful for pure synchronization and exceptions), and any, which permits all values to be sent or received (this allows gates to be "untyped", as in LOTOS, thus ensuring backward compatibility).

• A process is a program fragment that, as in LOTOS and other process calculi, executes and communicates with its environment by sending and/or receiving values on a set of gates.

Globally, LNT has four different kinds of routines, of increasing complexity:

• A constructor has only in parameters (call by value), no explicit definition, and does not raise exceptions.

• A pure function has only in parameters, an implicit or explicit definition, and may raise exceptions if needed (this provides for partially-defined functions).

• A procedural function (or procedure, for short) may have in, out (call by result), or in-out (call by value-result) parameters; unlike constructors and pure functions, it does not necessarily return a result; it usually has an explicit definition and may raise exceptions.

• A process may also have in, out, or in-out parameters; it has an explicit definition, may raise exceptions [START_REF] Garavel | On the Introduction of Exceptions in LOTOS[END_REF], and interacts with its environment by means of gates. The key difference between processes and other routines is that the execution of processes can be nondeterministic and let time elapse (the execution semantics is that of process calculi and labelled transition systems) whereas the three former kinds of routines execute deterministically and atomically (the execution semantics is that of functional languages).

LNT possesses three main concepts for denoting computation:

• An expression corresponds to the usual notion of expression in imperative programming languages. It is an algebraic term built using constants, variables, and calls to constructors and pure functions. The evaluation of each expression is deterministic (it always returns the same result or raises the same exception), atomic (it is expected to terminate and take a negligible amount of time), and free from side effects (it does not modify variables).

• An instruction corresponds to the usual notion of statement in imperative programming languages. Instructions serve to explicitly define the bodies of LNT functions. Basic instructions include: null (which does nothing), assignment to a variable or an array element, return of a function result, raise of an exception, procedure call, assert, etc. Instructions can be combined using structured-programming constructs, such as sequential composition, if-then-else conditionals, case with pattern matching, for and while loops, loops with break clauses, and declarations of variables with a limited scope. Because instructions manipulate and modify a store, the semantics of LNT relies on static analysis to prohibit all situations where uninitialized variables could be used; this way, instructions have an imperative-programming syntax and a functional-programming semantics. Like the evaluation of expressions, the execution of instructions is deterministic and atomic.

• A behaviour is the LNT equivalent of a LOTOS "behaviour expression". Behaviours serve to define the bodies of LNT processes. Behaviours can be seen as a superset of instructions since they contain all instructions (except return) but also include additional constructs specific to process calculi: stop (deadlock), communication on a gate (possibly with sending and/or receiving values), assignment of a non-deterministic value to a variable, process call, forever loop without break clause, nondeterministic choice (which is n-ary, rather than binary), parallel composition (which is n-ary and graphical [START_REF] Garavel | A Graphical Parallel Composition Operator for Process Algebras[END_REF], i.e., explicitly describes the communications/synchronizations between concurrent behaviours), gate hiding, and disruption (i.e., the "disable" operators of LOTOS). Unlike instructions, the execution of behaviours is nondeterministic, non-atomic, and may never terminate.

In the design of LNT, one main attainment is the integration in a single language of two very different models of computations: imperative/functional languages and process calculi. This was not the case with LOTOS, nor with its competitors Estelle and SDL, both of which clumsily amalgamate state machines with another formalism for data computation. Such a unification, which had been tried without success in E-LOTOS, is now effective in LNT. A key issue was the status of sequential composition [START_REF] Garavel | Revisiting Sequential Composition in Process Calculi[END_REF], which led to question and discard some well-established habits of process calculi, especially the action-prefix operator of CCS and LOTOS, and the use of dynamic semantics in place of static semantics.

Implementation of LNT

Contrary to the four aforementioned languages (Extended-LOTOS, Modular LOTOS, E-LOTOS, and LOTOS NT), the definition and implementation of which were planned as two successive steps (the latter being never undertaken or never completed), LNT was designed in a radically different way, using an "agile" approach. Every new language feature was first implemented and assessed on a growing base of non-regression tests before being adopted for LNT.

Initially designed as a standalone tool, the translator from LNT to LOTOS became an integral part of the CADP toolbox in 2010. Actually, this translator is not one single tool, but comprises three complementary tools:

• LPP3 ("LNT PreProcessor") is a small translator (2000 lines of C and Lex code) that expands the user-friendly LNT notations for literal constants (numbers, characters, strings, etc.) into algebraic terms making use of predefined LOTOS sorts and operations defined in custom libraries.

• LNT2LOTOS4 is a rather complex translator developed using the aforementioned SYNTAX/TRAIAN technology (3800 lines of SYNTAX code, 35,500 lines of LOTOS NT, and 2900 lines of C code). LNT2LOTOS translates an LNT specification into LOTOS code, possibly augmented with some little C code fragments.

• LNT.OPEN5 is a small utility (400 lines of shell script) that provides a top-level entry point for processing LNT specifications with the CADP tools and, more specifically, with the CAESAR.ADT [START_REF] Garavel | Compilation of LOTOS Abstract Data Types[END_REF] and CAESAR [START_REF] Garavel | Compilation and Verification of LO-TOS Specifications[END_REF] compilers for LOTOS, and the OPEN/CAESAR framework [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing[END_REF] for simulation, verification, and testing. Taking as input an LNT specification and an OPEN/CAESAR application program, LNT.OPEN first translates (the various modules composing) the LNT specification into LOTOS by calling LPP and LNT2LOTOS, then compiles the generated LOTOS specification by calling CAESAR.ADT and CAESAR, and finally invokes the OPEN/CAESAR application program to explore and analyze the corresponding state space on the fly.

Without exposing in full detail the algorithms implemented in LNT2LOTOS, these are some key principles underlying the translation:

• The main guideline is to keep the translation as simple as possible, so as to swiftly upgrade the translator each time the definition of LNT evolves. Consequently, duplication of work between the translator and the LOTOS compilers is avoided, meaning that the translator does not implement certain static semantics checks at the LNT level if the same checks are later performed at the LOTOS level. In particular, the translator makes no attempt to infer and check the types of LNT value expressions, deferring these tasks to the LOTOS compilers operating on the generated code.

• The channels used for typing LNT gates raise a specific problem because, on the one hand, the LNT2LOTOS translator is not intended to perform type checking and, on the other hand, LNT gates, which are typed, are translated into LOTOS gates, which are untyped, so that type-checking errors at the LNT level cannot be detected at the LOTOS level. To address this problem, LNT2LOTOS generates, for each LNT channel C, one or several overloaded LOTOS constant functions f C , which take as parameters the expected typed values specified for C and always return true. For each LNT action involving some gate G whose channel is C, a LOTOS Boolean guard is generated, which invokes function f C with the input or output offers of the action, thus expressing in LOTOS the typechecking constraints arising from the definition of C. If the action is not well-typed at the LNT level, the corresponding guard will provoke at the LOTOS level a type-checking error at compile time; otherwise, the guard will evaluate to true at run time.

• The LNT2LOTOS translator performs, on LNT functions and processes, static analyses not done at the LOTOS level; for instance, it rejects (or warns about) unused variables, variables used without being assigned before, variables assigned but never used, variables shared between concurrent processes, etc. Such checks are either required by the LNT semantics (see [START_REF] Garavel | Revisiting Sequential Composition in Process Calculi[END_REF] for a discussion) or suitable to ensure that LNT specifications remain as simple as possible, so as to increase readability and efficiency of verification.

• The predefined types of LNT (bool, nat, etc.) are implemented using base libraries written in LOTOS and C code. The user-defined types (built using free constructors or type combinators) are translated into LOTOS abstract data types (possibly with some additional C code meant for efficiency), together with their associated functions (equality, order relations, field accessors and selectors, etc.).

• Although, in LNT, user-defined functions and processes have the same functional/imperative style and share many constructs (e.g., assignments, assert, raise, if-then-else, pattern-matching case, for and while loops, loops with break, etc.), the two algorithms that translate, respectively, these functions and processes into LOTOS are very different, due to the fundamental asymmetry, in the target language, between the data part (based on abstract data types) and the behaviour part (based on process calculi).

• Our algorithm for translating LNT functions generalizes the one proposed in [START_REF] Ponsini | Rewriting of Imperative Programs into Logical Equations[END_REF], which translates into Horn clauses a small subset of C func-tions with only integer and list types. Our algorithm translates LNT functions into LOTOS (non-constructor) operations, which are defined using algebraic equations considered as conditional term-rewrite rules.

The translation takes advantage of the rewrite strategy implemented in the CAESAR.ADT compiler, which assumes a decreasing priority between equations. Notice that each LNT function having out parameters (call by result) or in-out parameters (call by value-result) translates to several LOTOS functions. The translation of certain LNT constructs (assert, case, and loops) also generates auxiliary LOTOS functions.

• Our algorithm for translating LNT processes takes its roots in our prior works on the translation to LOTOS of three modelling languages for hardware and software systems: the CHP2LOTOS translator [START_REF] Garavel | On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP[END_REF] for CHP, the FLAC translator [START_REF] Berthomieu | FIACRE: An Intermediate Language for Model Verification in the TOPCASED Environment[END_REF] for Fiacre, and the FSP2LOTOS translator [START_REF] Lang | Translating FSP into LOTOS and Networks of Automata[END_REF] for FSP. The algorithm is involved, but four main points are worth being highlighted.

(i) Certain behavioural LNT constructs directly map to equivalent LOTOS ones. For instance, each LNT gate translates to a corresponding LOTOS gate and each LNT process translates to a corresponding LOTOS process. The algorithm benefits from the fact that both LOTOS and LNT have an action-based (rather than state-based ) semantics and share a common semantic model (namely, labelled transition systems). Thanks to actionbased semantics, the translation can freely introduce auxiliary LOTOS processes and variables, still preserving the semantic model (which would not be possible with state-based semantics); in particular, execution traces are identical at the LOTOS and LNT levels, which avoids the usual need for a reverse translation of diagnostics from the target to the source level.

(ii) Certain behavioural LNT constructs are too powerful to be expressed using only the behaviour part of LOTOS; for such constructs, the data part of LOTOS must also be used, by generating auxiliary sorts, operations, and algebraic equations. For instance, the case construct present in LNT processes is translated using both the behaviour part of LOTOS (nondeterministic choice and Boolean guards are used to express the selection between the various case branches) and the data part of LOTOS (equations, considered as rewrite rules, are used to express pattern matching, which is not supported by the behaviour part of LOTOS).

(iii) An involved part of the algorithm translates the LNT parallel composition operator, which is n-ary, into an algebraic combination of LOTOS parallel composition operators, which are binary. Such a translation does not always succeed, meaning that certain network topologies specified in LNT cannot be expressed in LOTOS [START_REF] Garavel | A Graphical Parallel Composition Operator for Process Algebras[END_REF]; however, we never faced this problem in real-life case studies. Also, it was not possible to introduce in LNT the concept of n-among-m synchronization proposed in [START_REF] Garavel | A Graphical Parallel Composition Operator for Process Algebras[END_REF], because it is not supported in LOTOS; such a limitation is more annoying in practice, e.g., for the specification of Web services, which quite often require 2-among-m synchronization.

(iv) Another involved part of the algorithm translates the LNT sequential composition operator (which is unique, symmetric, atomic, and lets all values of variables assigned on its left-hand side flow implicitly to its right-hand side [START_REF] Garavel | Revisiting Sequential Composition in Process Calculi[END_REF]) into one of the two LOTOS sequential composition operators, either the action-prefix operator (which is asymmetric, atomic, and lets variable values flow implicitly from its left-to its right-hand side) or the "enable" operator (which is symmetric, non-atomic as it generates a τ -transition, and forbids variable values to flow from its left-to its right-hand side except if these variables are explicitly listed in an accept clause). Following the principles set for the CHP2LOTOS translator [START_REF] Garavel | On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP[END_REF], we chose to generate action prefix as much as possible and "enable" only when unavoidable, which produces better LOTOS code at the expense of a more involved translation. To fight state-space explosion and preserve strong equivalence between the LNT and LOTOS specifications, we slightly deviated from LOTOS semantics by adding a special pragma "(*! atomic *)" that instructs the LOTOS compiler not to generate a τ -transition when implementing the "enable" operator. There are many other algorithmic subtleties, such as the creation of auxiliary "continuation" processes for those LNT behaviours following loops and conditionals (i.e., case, if, and select), the translation of parallel composition occurring on the left-hand side of sequential composition where each parallel branch computes the values of different variables, the translation of out and in-out parameters of LNT processes into exit results returned by LOTOS processes, the need to respect the strict typing rules set by LO-TOS "functionality" constraints, the optimization of tail-recursive process instantiations, etc.

In addition to the above tools, which ultimately translate an LNT specification into a sequential C program, there also exists a compiler named DLC ("Distributed LNT Compiler") [START_REF] Evrard | Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes[END_REF][START_REF] Evrard | Automatic Distributed Code Generation from Formal Models of Asynchronous Processes Interacting by Multiway Rendezvous[END_REF] that translates an LNT specification into a set of C programs executing concurrently and communicating through TCP sockets; to produce such a distributed implementation, the DLC compiler exploits the concurrent architecture defined by the parallel composition operators present in the LNT specification.

Applications of LNT

The usability of the LNT language gradually increased with the progress of its translator to LOTOS. As of mid-2009, this translator was sufficiently complete and robust to allow a total shift from LOTOS to LNT at INRIA Grenoble, where no LOTOS code has been manually written since then, LNT being now the preferred high-level language for modelling concurrent systems and analyzing them using the CADP tools.

At Grenoble INP and Université Grenoble-Alpes, LNT has also replaced LOTOS to teach master students the fundamentals of concurrency theory. We observed that LNT enables students to better focus on high-level concepts, rather than getting lost in low-level details of LOTOS syntax and static semantics.

The LNT language and its tools have been used for many case studies, at INRIA Grenoble and in other academic or industrial labs as well (we only mention those not affiliated with the authors' institutions):

• Avionics: verification of an equipment failure management protocol 6 and of a ground-plane communication protocol 7 [START_REF] Garavel | Verification of GALS Systems by Combining Synchronous Languages and Process Calculi[END_REF][START_REF] Thivolle | Langages modernes pour la vérification des systèmes asynchrones[END_REF] provided by Airbus;

• Cloud computing: verification of self-configuration protocols • Human-computer interaction: specification and validation of graphical user interfaces for a prototype control room of a nuclear power plant 19 [85] and of plastic user interfaces exploiting domain ontologies 20 [20] (Toulouse, France);

• Industrial systems: model-based testing of the CANopen field bus and EnergyBus architecture 21 [54] (Saarland University, Germany), formal specification and rapid prototyping of a software controller for a metal processing plant 22 [START_REF] Garavel | The Unheralded Value of the Multiway Rendezvous: Illustration with the Production Cell Benchmark[END_REF].

Another indication of the practical usefulness of LNT is given by its use as a target language in a growing number of translators, which implement various languages by translating them to LNT. Indeed, LNT suitably replaces LOTOS for automatically-generated code as well as for handwritten code, since the translation to LNT is much easier than the translation to LOTOS, and because it is now preferable to let the LNT2LOTOS translator take in charge all algorithmic subtleties required to produce valid and efficient LOTOS code. We are aware of the following tools (again, we do not mention the authors' institutions):

• The BPMN2Py/Py2LNT translators23 [START_REF] Güdemann | Counterexample Guided Synthesis of Monitors for Realizability Enforcement[END_REF][START_REF] Poizat | Checking the Realizability of BPMN 2.0 Choreographies[END_REF] for analyzing choreographies of Web services specified in WS-CDL (Université de Nantes, France);

• The CMT translator [START_REF] Li | Improving Data Quality for Web Services Composition[END_REF] for the BPEL/WSDL specification languages for Web services (Tsinghua University, Beijing, China and MIT, Cambridge, MA, USA), and another, more complete algorithm for translating BPEL/WDSL/Xpath/XML Schema to LNT [START_REF] Thivolle | Langages modernes pour la vérification des systèmes asynchrones[END_REF];

• The DFTCalc tool24 [START_REF] Arnold | DFTCalc: A Tool for Efficient Fault Tree Analysis[END_REF][START_REF] Guck | DFTCalc: Reliability Centered Maintenance via Fault Tree Analysis[END_REF] for Dynamic Fault Trees (University of Twente, The Netherlands);

• The EB 3 2LNT translator 25 [100] for the EB 3 specification language for information systems (Université Paris Est, France);

• The GRL2LNT translator26 [START_REF] Jebali | Formal Modelling and Verification of GALS systems using GRL and CADP[END_REF] for the GRL specification language for GALS (Globally Asynchronous Locally Synchronous) systems;

• The OCARINA tool27 [START_REF] Mkaouar | From AADL Model to LNT Specification[END_REF] for the AADL architecture description language (ISAE, Toulouse, France and University of Sfax, Tunisia);

• The PIC2LNT translator28 [START_REF] Mateescu | PIC2LNT: Model Transformation for Model Checking and Applied Pi-Calculus[END_REF] for the applied π-calculus (an extension of the π-calculus with typed data values);

• the VBPMN translator29 [START_REF] Poizat | Checking Business Process Evolution[END_REF] for the BPMN language for describing business processes (Université Paris Ouest, France).

Conclusion

Computer systems handling asynchronous concurrency are inherently complex and cannot be reliably designed without adequate specification languages supported by sound analysis tools. Ed Brinksma contributed to this agenda in two significant ways: (i) by leading the definition and standardization of the LOTOS language, which exposed the key ideas of process calculi to a large audience and sparkled considerable interest in academia and industry; (ii) by sending a clear signal that LOTOS, despite its qualities, was not the end of the road and that further enhancements were possible and desirable.

The present paper provided a retrospective account of the evolution of the LOTOS-based family of specification languages, starting from LOTOS itself, reviewing the successive proposals for enhancing LOTOS (Extended LOTOS, Modular LOTOS, E-LOTOS, and LOTOS NT), and ending with LNT, the most recent descendent, which preserves the most valuable ideas of process calculi but entirely modifies the shape of the language to make it compatible with mainstream programming languages. The feedback acquired by using LNT for the design of complex industrial systems suggests that LNT provides a viable and effective replacement for LOTOS. Quoting STMicroelectronics engineers: "Although modeling the [Dynamic Task Dispatcher] in a classical formal specification language, such as LOTOS, is theoretically possible, using LNT made the development of a formal model practically feasible" [START_REF] Lantreibecq | Formal Analysis of a Hardware Dynamic Task Dispatcher with CADP[END_REF].

Concerning future work, we can highlight two main research directions:

• The LNT language is not yet frozen and can still be further enhanced.

For instance, the unification of exceptions across functions and processes is almost complete. We now consider equipping processes with optional return behaviours, so that functions become a strict subset of processes. We also plan to introduce, beyond assertions that already exist in LNT, pre-conditions, post-conditions, and loop invariants that would allow the application of mainstream theorem provers and static analyzers to LNT specifications.

• The current implementation of LNT by translation to LOTOS is justified by the reuse of existing LOTOS tools. It is intellectually challenging, but sometimes overly complex: for instance, LNT functions, written in a functional/imperative style, are first translated to LOTOS algebraic equations, and then compiled back to imperative C code. A native implementation of LNT would certainly be simpler and more efficient; it would also overcome certain LOTOS limitations that currently prevent useful constructs, such as the trap operator for exception catching [START_REF] Garavel | On the Introduction of Exceptions in LOTOS[END_REF] and the n-among-m synchronization pattern in parallel composition [START_REF] Garavel | A Graphical Parallel Composition Operator for Process Algebras[END_REF], from being added to LNT.

  Extended LOTOS breaks with the algebraic style of LOTOS and other process calculi by replacing unary and binary operators with n-ary constructs having a fully bracketed syntax, e.g., "sel B 1 [] B 2 [] ... [] B n endsel" for nondeterministic choice or "par B 1 || B 2 || ... || B n endpar" for parallel composition.

	• Extended LOTOS proposes other desirable features, among which a par
	operator ranging over a finite domain of values.

  Distributed algorithms: verification and performance evaluation of mutual exclusion protocols 11[START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF], verification of multiway synchronization protocols12 [START_REF] Evrard | Formal Verification of Distributed Branching Multiway Synchronization Protocols[END_REF][START_REF] Evrard | Génération automatique d'implémentation distribuée à partir de modèles formels de processus concurrents asynchrones[END_REF][START_REF] Evrard | Automatic Distributed Code Generation from Formal Models of Asynchronous Processes Interacting by Multiway Rendezvous[END_REF], specification and rapid prototyping of Stanford's RAFT distributed consensus algorithm 13[START_REF] Evrard | DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation[END_REF][START_REF] Evrard | Automatic Distributed Code Generation from Formal Models of Asynchronous Processes Interacting by Multiway Rendezvous[END_REF], and performance evaluation of concurrent data structures14 [102] (RWTH Aachen, Germany and Chinese Academy of Sciences, Beijing, China); • Hardware design: formal analysis and co-simulation of a dynamic task dispatcher 15 [70] (STMicroelectronics), formal analysis of ARM's ACE cache coherency protocol 16 [65, 66] (STMicroelectronics), verification and rapid prototyping of an asynchronous model of the Data Encryption Standard 17 [91], verification of a fault-tolerant routing algorithm for a networkon-chip 18 [103] (University of Utah, USA);

	8 [28] (Or-
	ange Labs), of the Synergy reconfiguration protocol for component-based
	systems 9 [8], and of dynamic management protocol for cloud applica-
	tions 10 [1];
	•

http://cadp.inria.fr

http://vasy.inria.fr/traian

http://cadp.inria.fr/man/lpp.html

http://cadp.inria.fr/man/lnt2lotos.html

http://cadp.inria.fr/man/lnt.open.html

http://cadp.inria.fr/software/12-e-choreography.html

http://cadp.inria.fr/software/12-i-dftcalc.html

http://cadp.inria.fr/software/13-a-eb3.html

http://cadp.inria.fr/software/14-c-grl.html

http://cadp.inria.fr/software/15-b-ocarina.html

http://cadp.inria.fr/software/13-d-pic2lnt.html

http://cadp.inria.fr/software/16-a-vbpmn.html


Romain Mesnil

teaching and research institutions in France or abroad, or from public or private research centers.


Maxime Bombrun

Vincent Barra

Andrew Harris

Analysis of thermal video for coarse to fine particles tracking in volcanic explosion plumes

Keywords: segmentation, feature extraction, contours, thermal imagery

This paper presents two algorithms of feature extraction and segmentation. The first algorithm is applied to detect tens of thousands of targets moving at high velocities (100's m/s) and with different sizes, velocities, shapes and directions. Upon detection, we compute statistics for each of these parameters for each particle, without any assumption nor a priori information. The second algorithm was developed to detect a slow moving convective cloud. The challenge was to follow the evolution of the contours of a heterogeneous element in front of a homogeneous but possibly moving background. These algorithms were applied on images acquired with thermal cameras with different settings (frame rate, frame size, focal length, instantaneous field of view). A case study concerning images of volcanic explosive events is finally presented. Volcanoes provide, during an eruption, a source of both ballistic ejecta and a convective plume of finer particles, gas and entrained air both of which can be imaged in the infrared wavelength. : Results ?

Introduction

The first infrared high-temporal-resolution system, operating at 20 images per second, was produced in 1965. However, the first hand-held system came with the introduction of high-spatial resolution focal plane arrays in 1993, and the first uncooled micro-bolometer-based system was produced in 1997. These developments, coupled with evolutions in high-speed digital electronics that allowed imagery to be stored on small memory disks "revolutionized the commercialization of thermal imaging systems" [START_REF] Holst | Common Sense Approach to Thermal Imaging[END_REF]. From here onwards, infrared imaging science expanded rapidly in many domains [START_REF] Kylili | Infrared thermography (IRT) applications for building diagnostics: A review[END_REF]. Thermal imaging cameras (TIC) produce a thermal image of a scene that provides information about both its temperature and radiative properties. Thus, TIC can be selected to be useful in multitude of hot spot tracking roles. Infrared Search and Track (IRST) systems were first developed for air defence applications [START_REF] De Jong | IRST and its perspective[END_REF]. Today, they are also used in civil applications, such as surveillance on land, at sea and in the air and warning against intruders [Fernandez-Caballero et al., 2011], survey danger areas where disasters may occur. IRST is also used in military applications. Thermal emission of gears operating on tanks or helicopters can, for example, be used to detect, track and lock-on to the target, so that many automatic target recognition (ATR) algorithms have been proposed [START_REF] Li | Experimental evaluation of FLIR ATR approaches -A comparative study[END_REF]. These segment and recognize vehicles, ships and aircrafts [e.g. [START_REF] Yilmaz | Target tracking in airborne forward looking infrared imagery[END_REF]. TIC can be selected in a wide range of applications, including fire control [START_REF] Amon | Thermal Imaging in Firefighting and Thermography Applications[END_REF], monitoring of buildings [START_REF] Kylili | Infrared thermography (IRT) applications for building diagnostics: A review[END_REF], medicine [START_REF] Arora | Effectiveness of a noninvasive digital infrared thermal imaging system in the detection of breast cancer[END_REF] and computer-aided diagnosis systems [START_REF] Faust | Application of infrared thermography in computer aided diagnosis[END_REF] or volcanology. In this case, one of the first field-based thermal measurement campaigns at an active volcano was completed by Thomas A. Jaggar [1917a,b]. He illustrated the benefits of remote thermal measurements against the common contact measurements, describing problems including equipment and personnel safety, and the limited measurement time available for a contact measurement imposed by the radiated heat from a lava lake. The first attempt to run a radiometer continuously was completed for a persistent degassing by [START_REF] Tazieff | New investigations on eruptive gases[END_REF] and during an explosive event by [START_REF] Shimozuru | Observation of volcanic eruption by an infrared radiation meter[END_REF]. Between 1965 and the end of 2007, at least 60 studies reported results obtained using ground-based broad-band radiometers for explosions, fumaroles and geothermally heated surfaces as well as lava flow, lakes and domes [START_REF] Harris | Thermal Remote Sensing of Active Volcanoes: A User's Manual[END_REF]. These applications of volcanological science achieved using thermal cameras were clustered in five main groups by [START_REF] Spampinato | Volcano surveillance using infrared cameras[END_REF]: hydrothermal areas and fumarole fields; lava bodies; explosive activity and volcanic plumes; pyroclastic flow deposits; fracturing and cracking. The most popular being the explosive activity (which accounted for 48 % of the studies published between 2001 and 2011). The key advance has been the ability to collect thermal video with spatial resolutions of a few centimeters and sampling frequencies of up to 120 Hz, with the operator being free to choose and modify the dynamic range, sampling rate, field of view, and targeted area, as well as acquisition start and stop times. Some of the first progress in the domain of volcanology to made were applications to track the dynamics of strombolian eruption plumes [START_REF] Dehn | Infrared Imaging of Strombolian Eruptions[END_REF]. In this paper, we aim to segment two major components of an explosive volcanic eruption using thermal video. First, we focused on all coarse particles as they exit the vent to gather parameters such as size, shape, velocity and mass for the solid (particulate) fraction of the plume, this being the contribution of particles with a diameter between 1 cm and 5 cm (lapilli-size) and between 6.5 cm to 35 cm (bombs-sized). We then analyzed the plume of gas and fine particles whose ascent will be buoyancy driven [START_REF] Turner | The starting plume in neutral surroundings[END_REF] and which can rise 100 meters up to over 25 000 meters above the vent. Thermal cameras have been used for plume tracking [START_REF] Spampinato | Volcano surveillance using infrared cameras[END_REF][START_REF] Valade | Plume Ascent Tracker: Interactive Matlab software for analysis of ascending plumes in image data[END_REF], however, the changing contrast between the optical properties of the emission and the background, and the evolution of plume properties over long time periods imply that the segmentation of volcanic plume remain a challenge.

1 Particle study (cm-sized analysis)

Methodology

The thermal camera used in this study was a forward looking infrared (FLIR). We used a FLIR Systems SC655, equipped with a 3.6× magnification lens and recording at 200 frames per second. The focal length was 88.9 mm and the IFOV was 0.19 mrad. Our acquisition frequency. We note that our frames usually have a size 600 × 480 pixels, but are automatically truncated to allow recording at rates greater than 30 Hz; for example, at 200 Hz, the image size is 600 × 120 pixels. This resizing is automatically performed by the acquisition software and the resized frame is centered on the same pixel as the large frame and the spatial resolution does not change. The spatial resolution (or pixel dimension, L p ) will depend on the detector instantaneous field of view (IFOV), which is defined by a cone opening at angle β IF OV , and the distance to the target (D), so that the pixel diameter is given by L p = 2[Dtan(β IF OV /2)] = D × β IF OV , using paraxial approximation defined for the small angle. Given the large number of particles expected and the quantity of data recorded by the thermal camera (two hundred 640 × 120 pixel images, 150 kB in size every second or 1.8 GB per minute), we opted for a simple, yet-effective algorithm to extract particle parameters. A first step is to remove the static objects of the image, this being the static background, i.e. a set of components from the image prior to the event. The static background can usually be removed by preprocessing approaches, as reviewed in [START_REF] Brutzer | Evaluation of background subtraction techniques for video surveillance[END_REF]. Given the time of the beginning of the event (t = 0), the easiest way to remove the static background is to consider the difference between the current frame I t and a reference frame acquired before the event, termed the "background image", I t<0 or I Ref . Once the static background was removed, we focused on the moving part of the video. The positions of the particles on the images were detected by subtracting the previous frame I t-1 from the current frame I t . However, all moving elements are detected by this process, including those we did not want to detect (e.g., birds, insects). This is termed the "dynamic background". To solve for this, a first differentiated image at time t (T t ) is generated,

T t = I t - αI t-1 + γI Ref α + γ ∀ t ∈ {1, n} (1)
where α and γ are weights derived empirically which change according to the predominance of the static versus dynamic background, those being not independent. In the image, only particles and a low intensity hint of the background persist. Because we only want to detect components among the brightest features, we process F t = T t • 1 1 {It-I0≥th} using a New White Top-Hat transform [START_REF] Bai | Analysis of new top-hat transformation and the application for infrared dim small target detection[END_REF]:

M N W T H = f -min(((f ⊕ ∆B) B b ), f ) (2)
where ⊕ is the dilation operator and the erosion operator. Parameters ∆B and B b are both square-shaped structuring elements. We apply a 21 pixel diameter box with, following Bai and Zhou [2010], a three-pixel wide perimeter for ∆B.

That is, pixels in the central 15-pixel-wide box have values of zero, and the three-pixel-wide perimeter have values of one.

The second part of the algorithm tracks each particle through time. This allows us to compute the velocity of each particle but also to clean up false detections which may have been occurred during the segmentation process, these being those without matching positions. We chose the maximum intensity pixel of the target as the initial position with subpixel accuracy following Shindler et al.

[2010]. Now, ω i,t = (x i,t , y i,t ) is the subpixel-position of particle i at time t.

We defined the velocity of the particle in the image plane by the pixel distance traveled by the particle between two consecutive frames separated by time t:

U i,t = ω i,t+1 -ω i,t (t + 1) -t ; (3)
The position of particle i at time t + 1 can now be estimated following several conditions (spatial, intensity, trajectory). We then estimated the velocity in meters per second assuming a planar projection. We also used the radius of the short axis r S and the radius of the long axis r L to compute the width of the particle i as an average radius r = r S +r L

2

. The volume (V i ) is then computed assuming a prolate spheroid, so that V i = (4/3)πr 2 S r L . Finally, given an appropriate density, particle volume can be converted to mass m i . This algorithm was tested and validated on an artificial experiment [START_REF] Bombrun | Algorithm for particle detection and parameterization in high-frame-rate thermal video[END_REF]).

Natural case

The algorithm was tested on videos containing high velocity particles imaged at Stromboli volcano (Aeolian Islands, Italy). In 2012, we completed eight hours of recording spread over four days spanning 27 September-5 October during which time we recorded 13 eruptions. In 2014, we recorded for eight hours on 17 and 18 May, capturing a further 18 events. We set up our high speed camera at Pizzo Sopra la Fossa, a natural platform which overlooks Stromboli's active crater terrace and at a distance of 280 m from the active vent, tilted downwards at an angle of -23 degree. At this distance, we can detect particles down to 5.5 cm. Emission durations ranged from 5 s to 50 s, with an average of 14. The number of particles ejected during single events detected ranged from 610 to 5 320 with an average of 2 685. A total of 83 220 particles were detected for all 31 eruptions. The particle size distribution reveals that the majority of the particles (67 %) are between the lower limit, 5.5 cm, and 10 cm with a mean particle width of 10 cm and a standard deviation of 5.6 cm. We assess particle shape in terms of the following normalized shape index: (r L -r S )/(r L +r S ). Using this index, a perfectly oblate shape will have a value of -1/3 whereas a perfectly prolate shape will have a value of +1/3; a perfect sphere will have a value of 0. We found that only 17 % of our particles approximate a spherical shape. Of the remaining 83 %, 29 % are oblate and 54 % are prolate. The dominance of the prolate shape is consistent with deformation or stretching in the direction of motion. We used the density of samples, from lapilli to bomb size as collected during campaigns in 2008 [Coló, 2012;[START_REF] Gurioli | Dynamics of Strombolian explosions: Inferences from field and laboratory studies of erupted bombs from Stromboli volcano[END_REF], 2010 [START_REF] Gurioli | Classification, landing distribution, and associated flight parameters for a bomb field emplaced during a single major explosion at Stromboli, Italy[END_REF] and 2011 [START_REF] Leduc | Types and mechanisms of strombolian explosions: characterization of a gas-dominated explosion at Stromboli[END_REF] to compute the mass of each particle and the total mass ejected during the eruption. Erupted masses erupted range between 1 270 kg and 11 820 kg with a mean of 4 585 kg. The particle mass distribution revealed that most particles have a low mass, where 46 310 (or 56 %) of all of the detected particles had a mass of less than 4 kg. This population accounts for 10 220 kg or 4.6 % of the total mass. However, the 2 524 particles greater than 25 cm (3 % of the total detected particles) account for 44 % of the total mass. The velocity distribution had a mode between 20 m/s and 30 m/s, with an average velocity of 45 m/s on which the standard deviation was 36 m/s. Particle velocities at Stromboli are generally less than 100 m/s [START_REF] Chouet | Photoballistics of volcanic jet activity at Stromboli[END_REF][START_REF] Patrick | Strombolian explosive styles and source conditions: insights from thermal (FLIR) video[END_REF]. Here, 91 % of all of particles measured had velocities of less than 100 m/s. However, 7 330 particles (8.8 %) had velocities greater than 100 m/s and up to 240 m/s. This approaches the higher velocities recently found for normal explosion at Stromboli by [START_REF] Taddeucci | High-speed imaging of Strombolian explosions: The ejection velocity of pyroclasts[END_REF], Delle Donne and Ripepe [2012] and [START_REF] Harris | Detailed analysis of particle launch velocities, size distributions and gas densities during normal explosions at Stromboli[END_REF]. Finally, considering the large number of particles detected (83 220), the impact of outliers is vanishingly small. We concluded that our dataset is statistically robust. Full data sets and overview statistics are given in Bombrun et al. [2015].

2 Plume study (meter-sized analysis)

Target

Our primary objective was to develop an operational algorithm capable of detecting a moving plume through time. A volcanic plume is a mixture of particles, gases, and entrained atmospheric air, which are injected into the atmosphere during a volcanic explosion [START_REF] Carey | Volcanic plumes. Encyclopedia of volcanoes[END_REF]]. Thus, the camera used for the plume study was a FLIR Systems SC660. Such volcanic plumes are slow moving targets which may be dispersed on both local and global scales so that frame rates of 1 Hz are more than adequate. The first step of the algorithm was to consider the differentiation (D t,t-step ) between the current frame (I t ) and the previous frame (I t-step ). We applied a single level discrete 2-D wavelet transformation, using a Daubechies wavelet (db1), on the absolute value of D t,t-1 . We computed the approximation coefficient matrix to perform a direct reconstruction from the 2-D wavelet coefficient. From the absolute value of the reconstructed image, we computed a single threshold for the image using Otsu's method [START_REF] Otsu | A Threshold Selection Method from Gray-Level Histograms[END_REF] to obtained a partial mask of the plume. We cleaned this mask by applying a morphological opening transformation with a 1 pixel radius disk and removing detected elements less than 5 pixels in area.

We completed this mask by performing the same process with another differentiation, D t,Ref , this being the difference between the current frame (I t ) and a reference frame recorded before the event (I Ref ). We summed the two masks to obtain the final differentiated mask. However, because the wavelet transformation was coarse, we needed to redefine the edges. Thus, in the next step, we performed a morphological reconstruction, i.e., we applied a repeated dilatation process to the mask until its contour fitted the original image, I t . Each successive dilation was constrained to lie underneath I t . We cleaned the final image by removing outliers and we computed the contour using a Canny edge detector.

Applications

We first tested the algorithm on thermal video for the ascent of a volcanic ash plume at Santiaguito volcano, Guatemala. This video was recorded in 2005 and the emission duration is 170 s (i.e. 5 100 frames). The background was composed of a homogeneous sky with weak-intensity meteorological clouds, and the ground contrasts with the plume with a weak-intensity lava flow being apparent on the left side of the vent. Unfortunately the algorithm was too efficient regarding the low contrast image elements so that some meterological clouds were detected as a part of the plume. We removed clouds not pixel-connected with the plume by considering the largest component and improved the contrast by using wavelets on the differentiated image as a pre-processing step.

The second video was recorded at Stromboli volcano, Italy in May the 28 th 2012. The camera was set up at Pizzo Sopra la Fossa and pointed at the North-East crater over a direct distance of 300 m so that the image covered a height of 308 m. Plume emission lasted 67 s (i.e. 2 000 frames). The background was a homogeneous sky and cold ground around the vent with another vent on the left which produced unwanted detection. The distance between the camera and the vent was shorter than at Santiaguito, thus the impact of the heat radiated by the crater was more problematic. During plume ascent, the overturn convection continually brought hot spots to the front of the plume creating a random intensity in the plume and making intensity tracking difficult.

The third video was recorded at an experimental facility near Buffalo, USA. The University at Buffalo completed experiments that use small chemical explosive charges buried in layered aggregates to simulate the effects of subsurface hydrothermal and phreatomagmatic explosions [Valentine et al., 2015]. At the same time, three more powerful blasts were performed. These released a plume of fine sand particles. The blast used to test our algorithm was that of Pad 5, Blast 4. The energy produced by the explosion was 2.30 × 10 6 J and the depth below the surface was 0.5 m. The camera was set up XXXX m from the source so that the field of view was XXXX m height. The ambiant background was composed of trees at ambiant temperature, moving with the wind to create a moving background. The top of the video comprised sky that had a huge contrast with the threes. This video was the most difficult to process due to the numerous and contrasting features in the video. At this point, a global threshold or a double threshold were not solutions anymore. The last video was recorded at an experimental facility near Munich, Germany, where the Ludwig-Maximilians University completed large-scale ash settling experiments. Natural basaltic ash (0 -500 µm) was released with different controlled volumetric flow rates in a shock tube system. The experiment used to test our algorithm was the #33. The sample came from Monte Rossi Scoria (Italy), it was fully water saturated, the sample porosity was 30 % and its volume was 29.44 cm 3 . The pressure of the decompression was 15 Mpa. The camera was set up horizontally at a distance of 4 m so that the field of view was 4.6 m height.

Conclusion

We present, new approaches to deal with segmentation and feature extraction in thermal video. The first algorithm detects, tracks and parameterizes small dim targets in high-speed IR videos. Based on a mathematical morphology transformation hybridized with refinement by thresholding, this method allowed us to obtain a statistically robust database of 83 000 particles emitted during explosions at Stromboli volcano. Statistically, most of the particles have sizes between 5 and 15 cm, and the majority of individual particle masses are below 0.5 kg. The particle velocity distribution is positively skewed with a mode between 20 and 30 m/s. The second algorithm detected and tracked fine particles in plumes moving across large field of view IR video frames. This method is based on a background subtraction by Daubechies wavelet transformation with a refinement by image reconstruction. It was tested on several cases with different levels of difficulties.

We applied it to a volcanic plume in which the heat of the crater restricted the use of a global thresholding and on controlled/experimental explosions in which the background was more complex (moving trees, hot spot created by warm electronic components, etc.). This algorithm proved to be robust enough to detect these plumes despite of the complex image background. These two algorithms are designed to provide necessary information to allow improved understanding and modeling of dynamics during volcanic explosions. Statistically robust databases for vent-leaving particle dynamics remain scarce. Thus, the ability to measure the dynamics of volcanic emissions as they exit the vent and the computation of the particle parameters is an excellent way to understand the dynamics related to the fragmentation and particle emission processes. At the same time, using algorithm output to compute plume parameters such as height, front velocity and spreading angle could be used to constrain models that describe the source geometry and height of volcanic jets [e.g., Jessop and Jellinek, 2014].

NE C

Fig. 1 :

 1 Fig. 1: Overview of the three main craters at Stromboli from Pizzo Sopra la Fossa where the cameras were set up.

  Fig. 2: XX

Fig. 5 :

 5 Fig. 5: XX

Acknowledgments

This research was financed by the French Government Laboratory of Excellence initiative nXXX ANR-10-LABX-0006, the Rgion Auvergne and the European Community.