DEPLOY

Objectives

The overall objective of DEPLOY is to make major advances in the industrial practices of engineering for dependable systems, through the deployment of formal engineering methods and tools.

Industries are facing the challenges of mastering the development of ever more complex systems with ever higher assurance. Formal engineering methods provide an answer to both of these challenges through precise modelling of the system, powerful reasoning support for the models (using automated analysis tools such as theorem provers and model checkers), and afterwards exploitation in domainspecific models and code generation.

Industries are now increasingly considering formal engineering methods. DEPLOY aims at overcoming problems of integrating these methods into industrial development lifecycles, and at presenting evidence of their overall efficiency and benefits in order to foster their adoption.

Project Results

Throughout the lifetime of the project, DEPLOY methods and tools were intensively deployed in real industrial settings by the industrial partners of 4 major sectors in order to test them against the industrial imperatives of cost-effectiveness, scaling and ability to cope with evolution of requirements. The main outcome are the following:

• Methodological guides, training plans, experience report on the industrial application of formal methods and tools
• Industrial extension to the method especially to manage requirements, reason on dependability, support verification and validation, especially using proof and model-checking techniques
• Extension to the RODIN Open Source platform in order to answer industrial needs in terms of robustness, user-friendly interface and modularity.
• Production of an industrial Frequently Asked Questions for the adoption or formal engineering methods.

Value Added for Enterprises

For industrial partners achieving greater system dependability is essential to maintaining the competitive edge they currently enjoy through their excellence in engineering. DEPLOY provided a validated methodology to introduce formal engineering techniques in a controlled and measurable way, based on large scale experiments conducted simultaneously deployment in five major industrial sectors whose core business is the construction of safety-critical, business-critical and mission-critical systems. Such systems are required to have a high degree of dependability.

DEPLOY also produced a professional Open Source development environment for formal engineering methods and because the industrial deployment partners are committed to further improvement of their development processes. The professional development environment was built on the existing successful Eclipse-based RODIN environment.

Particular engineering problems for the industrial partners include the difficulty of requirements validation, the rapidly-growing complexity of system testing, the difficulty of maintaining quality and safety of systems under evolution and the problems caused by trying to integrate components of diverse origin. DEPLOY addressed all these issues, helping the industrial partners to achieve real improvements in their engineering processes and, in the longer term, is leading to improvements in European industrial practice more generally.