Keywords formal methods, software validation, safety-critical software
Start Date: 01-JUL-90 / Duration: 51 months
[ contact / participants ]
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:
The strategic approach is to:
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.
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.
Mr Chris George
DK - 3460 BIRKERØD
tel: + 45/ 45-822-100
fax: + 45/ 45-821-766
telex: 16066 CRI DK
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
LACOS - 5383, December 1993
please address enquiries to the ESPRIT Information Desk
html version of synopsis by Nick Cook