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.
The objectives of the project were:
The EASEL project undertook the following case studies. Hypertext links indicate where more detailed information can be found.
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.
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.
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.
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).
Ken Turner (British Coordinator)
Ji He (Helen Ji)
Tomás Robles (Spanish Coordinator)
Up one level to Ken Turner - Research ProjectsLast Update: 15th July 2006