E-LOTOS: Tutorial and Semantics

Alberto Verdejo

Master's Thesis, June 1999.

Abstract:

Part I

This tutorial introduces E-LOTOS by describing all the features of the language, and by showing its expressive power. We show how E-LOTOS can be used to specify systems, their behaviour, and the values they manipulate, as well as how the specifier can modularize systems. The tutorial includes some small examples that show how E-LOTOS features are used to specify common problems, usual generic data types, well-known concurrent programming problems, as well as to describe hardware components.
E-LOTOS is still a draft, under revision. So this is still an unfinished document, it has to be completed when the ISO standard will be definitively approved.

Part II

In this part we define and explain the E-LOTOS semantics. In Chapter 6 we give the translation from the concrete syntax, used to write the specifications, to the abstract syntax, used to define the semantics.
In Chapter 7 we define the static semantics of the Base Language, that defines which \elotos terms (in the abstract syntax) are semantically correct, and in Chapter 8 we show the dynamic semantics, that defines how an \elotos specification can evolve. In Chapter 9 we show the semantics of a simple module system.
We have followed the semantics introduced in [Que98] as much as possible. However, [Que98] is a draft and is still being revised. From our point of view, it suffers from some problems which are being discussed. In this report we give our proposed solution to these problems.

[Que98] J. Quemada, editor. Final committee draft on Enhancements to LOTOS. ISO/IEC JTC1/SC21/WG7 Project 1.21.20.2.3., May 1998.

[pdf]

@MastersThesis{Verdejo99,
  author =       {Alberto Verdejo},
  title =        {{E-LOTOS: Tutorial and semantics}},
  school =       {Departamento de Sistemas Inform\'aticos y Programaci\'on,
                  Universidad Complutense de Madrid},
  year =         1999
}