Large-Scale Correct Systems Using Formal Methods


LACOS - 5383

Keywords formal methods, software validation, safety-critical software


Start Date: 01-JUL-90 / Duration: 51 months

[ contact / participants ]


Objectives

Formal methods for software engineering have an important role to play in producing correct software systems, especially in areas such as space and defence, and in control and monitoring systems that are safety-critical. Such methods are becoming available to industry, with tool support, documentation and training material. A prime example of this development is project 315, RAISE, that has successfully completed the development of the formal specification language RSL, its methodology and an extensive tool-set. RAISE addresses a lot of applications areas. It provides a single framework for specification and design, and a range of formal and informal development techniques.

Generally speaking, industry still needs evidence that formal methods can be used in large applications in practice. The aim of the LACOS project is to establish and demonstrate formal methods, specifically RAISE, as a viable industrial technique in the scalable production of large, correct IT systems. The effect (compared with current methods) will be:

Approach

The strategic approach is to:

Progress and Results

In the first phase, the emphasis has been on conducting a wide range of applications in different industrial areas, using existing and evolving technology from RAISE, analysing experience, proposing and implementing enhancements, and thus evolving RAISE technology.

In the second phase, the emphasis is on standardisation, demonstration (by applications), industrialisation of support tools and documentation, and widespread publicity.

Exploitation

All of the partners are involved in the production and marketing of software systems, most of them directly. Formal methods have been established and used by the partners in order to increase the productivity of correct information systems development. RAISE is being used in various ways, and in particular in the development of systems now becoming commercially available, and in the investigation of the detailed design of difficult areas of systems under development, both as part of the design process and as a means of investigating existing designs by reverse engineering.

The RAISE technology is being marketed commercially both in Europe and North America. A book on the RAISE Specification Language has been produced and published, as well as papers published in journals and presented at conferences. A video training course has also been produced. Exploitation will continue with further tool enhancements, publications and publicly available courses.


CONTACT POINT

Mr Chris George
CRI A/S
Bregnerødvej 144
DK - 3460 BIRKERØD
tel: + 45/ 45-822-100
fax: + 45/ 45-821-766
telex: 16066 CRI DK
email: cwg@csd.cri.dk

Participants

CRI A/S - DK - C
BULL SA - F - P
MATRA TRANSPORT - F - P
BNR EUROPE LTD - UK - P
TECHNISYSTEMS LTD - GR - P
CAP PROGRAMMATOR A/S - DK - P
SPACE SOFTWARE ITALIA SPA - I - P
LLOYD'S REGISTER OF SHIPPING - UK - P
INISEL - E - P


ST synopses home page ST acronym index ST number index
All synopses home page all acronyms index all numbers index

LACOS - 5383, December 1993


please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook