Keywords formal description techniques, LOTOS, technology transfer
Start Date: 01-APR-89 / Duration: 36 months
[ contact / participants ]
The aim of the LOTOSPHERE project was to foster the exploitation by industry of mathematically sound formal design techniques. This was to be achieved by project engineering and by using a viable, fully tool-supported, formal system design and development methodology.
The methodology was centred on the emerging international standard Formal Description Technique (FDT) LOTOS (IS8807). The LOTOSPHERE project intended to convert LOTOS into an industrial tool applicable to system design and system implementation. This included the development of design structuring techniques, integrity-preserving transformations, a test theory and methods, language enhancements, and an integrated toolset. These methods and tools will be applied to industrial pilot specifications and implementations.
Until now FDTs have been primarily developed and used with the objective of reporting the architectural design and specification phase. The aim has been the development of correct, implementation-independent specifications that faithfully reflect an architecture. LOTOS is a particularly flexible and expressive FDT which can support a variety of specification styles (object-oriented, constraint-oriented, etc). This makes LOTOS a natural and appropriate foundation on which to base high-quality software engineering of concurrent and distributed systems. Such a LOTOS environment will support the entire implementation path, thus permitting the rapid development of correct and high-quality implementations from architectural specifications.
In general terms, the current worldwide success of the LOTOS language (currently LOTOS represent 80% of the worldwide R&D activity in functional description techniques), the enlargement of the LOTOS community, the LOTOS standards, which have finally emerged in ISO and in CCITT, and the 23 CEC projects based on LOTOS, are a direct consequence of the intense activity led by the LOTOSPHERE project members.
More specifically: the design structuring methodology has been developed and described in different ways to show its merits to different audiences; a catalogue of LOTOS-to-LOTOS transformations has been compiled. Every transformation can be used as a design step or part of a design step within the methodology; testing methods have been assessed, a test derivation methods has been investigated, test selection and description assessed, and the practical relevance of these LOTOS-based methods determined; the first proposals for LOTOS enhancements have been made by means of test-bed experiments to improve the language's industrial applicability; several versions of a toolset have been distributed to all partners, incorporating: elementary LOTOS editing and simulation tools; tools to support verification; tools to support transformations; and tools to support compilation. They enable, for example, testing by simulation and/or compilation as well as verification. A user manual for the toolset has been made; and for all applications, realistic implementation-independent specifications have been made, which serve as a basis for designing and providing the first feedback on methodology, language and tools.
The successful completion of the project represents a major advance in the industrial use of LOTOS. This will significantly enhance the activity of several European IT companies in providing quality software of verifiable functionality, and place them at the forefront of formal methods applications worldwide. The academic partners of LOTOSPHERE further develop new methods and tools to support system design based on LOTOS. A company (Information Technology Architecture B.V.) exploits the tools and distributes these tools and updated versions successfully. Some industrial partners apply the LOTOSPHERE methods and tools in pilot projects. A book on the main project results has been prepared and could be published next year.
Prof Chris A. Vissers
UNIVERSITEIT VAN TWENTE
Computer Science Department
NL - 7500 AE ENSCHEDE
tel: + 31/ 53-893792
fax: + 31/ 53-333815
telex: 44200 UT NL
UNIVERSITEIT VAN TWENTE - NL - C
ALCATEL STANDARD ELECTRICA SA - E - P
BRITISH TELECOMMUNICATIONS PLC - UK - P
CPR - I - P
GMD - D - P
INRIA - F - P
OCE-NEDERLAND BV - NL - P
TECHNISCHE UNIVERSITÄT BERLIN - D - P
UNIVERSITY OF STIRLING - UK - P
UNIVERSIDAD POLITECNICA DE MADRID - E - P
SYSECA - F - P
CNRS-LAAS - F - P
PTT RESEARCH NEHER LABORATORIES - NL - P
ASCOM HOLDING LTD - CH - P
CNR-CNUCE - I - A
CNR-IEI - I - A
LOTOSPHERE - 2304, December 1993
please address enquiries to the ESPRIT Information Desk
html version of synopsis by Nick Cook