EASEL Project
(Evaluating And Standardising Enhanced LOTOS)

Introduction
Objectives
Case Studies
Project Team

Introduction

EASEL (Spanish: CABALLETE) was undertaken from April 1998 to August 2000, funded by the British Council and the Ministerio de Educación y Cultura under grant 2246. The goal was to support the development and uptake of the formal language E-LOTOS (Enhancements to LOTOS) that was being standardised internationally by ISO. E-LOTOS is intended for the precise specification of computing and telecommunications systems. Case studies were undertaken using E-LOTOS in areas such as communications protocols, distributed systems and hardware-software co-design.

LOTOS (Language Of Temporal Ordering Specification, ISO 8807) is an important international standard for formal development of computing and telecommunications systems. Although originally conceived for describing standards from OSI (Open Systems Interconnection), LOTOS has been widely used in a number of other areas.

Relative to the original version of LOTOS, E-LOTOS offers important new features that are industrially significant and improve its usability in many areas. These new features are a response to extensive trials and applications. Experience with the original version of LOTOS showed that it is very important to conduct realistic trials during language development. E-LOTOS will benefit from the results of such trials. Experience also showed that E-LOTOS needed a convincing portfolio of case studies to encourage industrial uptake and effective use of the language.

Objectives

The objectives of the project were:

to support the development and use of E-LOTOS (ISO JTC1/SC21/WG7)
to enhance the design of the language by conducting realistic case studies and feeding improvements in the language back into the standardisation process
to make the language more (industrially) usable by preparing a portfolio of case studies that show how to use the language successfully on realistic applications
to contribute to the final stage of standardising E-LOTOS by providing feedback from the point of view of real users
to contribute to a future text-book on E-LOTOS

Case Studies

The EASEL project undertook the following case studies. Hypertext links indicate where more detailed information can be found.

E-LOTOS Tutorial
This tutorial introduces E-LOTOS to the beginner, including a number of small examples as well as some more realistic ones.
The tutorial was written by Alberto Verdejo and reviewed by Ken Turner. The tutorial is available as compressed PostScript or PDF.
Invoicing System
This case study investigated the use of E-LOTOS for the invoicing system proposed by Henri Habrias (University of Nantes). As a relatively simple problem, this example demonstrated the use of E-LOTOS without the complications of a realistically sized problem. For comparison, data-oriented and process-oriented specifications were developed in E-LOTOS. Equivalent specifications were also developed in LOTOS to show the advantages to be gained from using E-LOTOS.
The case study was specified by Ken Turner and is available as PDF. Joint work was also undertaken with Mihaela Sighireanu (then of INRIA Rhône-Alpes) on the verification of the case study. This led to the publication of an INRIA Research Report, available as PDF.
Hardware Description
This case study investigated the use of E-LOTOS for specifying hardware. The new language features for data typing, modularity and timing were studied to see how they applied to the description of asynchronous and synchronous hardware designs. Validation and verification of functional and timing aspects were carried out (within the constraints of available tools).
The case study was specified by Alberto Verdejo. The main outcome of the study appears in the E-LOTOS tutorial. Ji He also undertook additional work on specifying digital hardware. A paper on the specification of synchronous hardware is available as PDF. A paper on test generation for synchronous hardware is available as PDF. Verification of asynchronous hardware is discussed in a paper available as compressed PDF. Further information can be found in the description of the DILL project.
FireWire (Serial Multimedia Bus)
This case study investigated the use of E-LOTOS for the specification of the tree identify protocol (a leader election protocol that forms an important part of the IEEE FireWire bus standard). Specifications were developed at various levels of abstraction, partly to indicate how E-LOTOS can be used, and partly to show how the protocol can be progressively elaborated.
The case study was specified by Carron Shankland and reviewed by Alberto Verdejo. It is described in a paper available as PDF.
Telecommunications Services
This case study investigated the use of E-LOTOS for the specification of telecommunications services such as those found in the IN (Intelligent Network). One aspect that was investigated is how the new data typing and modularity mechanisms of E-LOTOS could be exploited to give clearer and more usable specifications. Another aspect that was investigated is how the timing facilities of E-LOTOS could be used to specify telecommunications services that are time-dependent (such as One Number and Call Forwarding on Busy Line).