Promotion of Formal Methods in the European Software Industry

PROOFS - 5342

Keywords formal methods, distributed systems

Start Date: 01-DEC-90 / Duration: 30 months

[ contact / participants ]

Objectives and Approach

The PROOFS project had the initial objective of stimulating and promoting the use of formal techniques for heterogeneous distributed applications. PROOFS wanted to develop a generic technology which should be adaptable to the different application domains targeted by the project: banking (credit and bank loan authorisation), finance (electronic shopping with integrated back office) logistics (logistic support in a transport company) and telecommunication (document teleconferencing system)

Demonstrations on real industrial application pilots were planned to asses the PROOFS developments. The development of a specific training material was also planned to allow the technology transfer towards the development teams of the specific application domains

The project has addressed the fact that distributed applications are becoming more and more complex. In consequence, their integration creates an increasing need for methods to reduce the cost of development and maintenance and to allow the reusability of components already developed.

The work has been directed by the following application needs:

• Integration at the application level:
  • defining a distributed application
  • early validation of concepts with customers from different backgrounds and of architectures integrating communication flows between already existing heterogeneous systems and network architectures.
• Integration at the technical level:
  • use of formal methods to increase reliability, reusability, and maintainability
  • generality, in order to factorise developments, reduce the cost of the needed environment, standardise throughout different application domains and provide a bridge between all players.

Progress and Results

The project, launched in December 1990 with a planned duration of 4 years, did not obtain further funding after 30 months because of budget constraints within ESPRIT. The actual results of PROOFS that will be used after the project and that can be industrially exploited are:

• A method adapted to the development of distributed heterogeneous systems that covers the application life cycle from requirement analysis to coding. This method results from background methods and techniques brought by the technology provider partners and from the requirements and feedback of the application providers. Along with this method, corresponding formalisms and techniques have been agreed to support the design of application.
• Extension and improvements of selected tools has been done. In particular, the ExSpect tool and CGE/XNIAM have been concerned. This work has allowed a technology transfer of ExSpect to a software house, that is now commercialising the tool. The integration of these tools has also been started to fully support the PROOFS method.
• Experiments made on real applications that have demonstrated the feasibility of the PROOFS approach. These experiments have allowed the partner to design the method, to improve the tools and also have motivated further studies by the application providers mostly in the field of requirements analysis.
• A set of training material designed to support the PROOFS method and the utilisation of the techniques and tools developed in the project.

CONTACT POINT

Mr Sergio Copelli
c/o PRISMA INFORMATICA SPA
Villa dell'Ombre
Piazza di Bellosguardo 11
I - 50124 FIRENZE
tel: + 39/ 55 223 021
fax: + 39/ 55 229 020

Participants

PRISMA INFORMATICA SPA - I - C
TECHNISCHE UNIVERSITEIT EINDHOVEN - NL - P
SLIGOS SA - F - P
TELESYSTEMES - F - P
INSTITUTE ITP TUE-TNO - NL - P
ENTEL SA - E - P
TNO - NL - A
MASI - F - A
ALCATEL - ISR - F - P

PROOFS - 5342, December 1993

please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook