About Deploy Project

Concept and Project Objective

n this section we explain the aims of DEPLOY and outline its motivation and expected outcomes.

Summary of DEPLOY

As highlighted by the FP7 ICT Workprogramme, the order of magnitude increase in the complexity of future systems over today’s systems poses major new engineering challenges. The increase in complexity means that achieving dependability of future systems will require huge advances in system engineering methods. The overall aim of the DEPLOY Project is to make major advances in engineering methods for dependable systems through the deployment of formal engineering methods. Formal engineering methods enable greater mastery of complexity than found in traditional software engineering processes. It is the central role played by mechanically-analysed formal models throughout the system development flow that enables mastery of complexity. As well as leading to big improvements in system dependability, greater mastery of complexity also leads to greater productivity by reducing the expensive test-debug-rework cycle and by facilitating increased reuse of software.

The work of the project will centre on, and be driven by, the tasks of achieving and evaluating industrial take-up, initially by DEPLOY's industrial partners, of the DEPLOY's methods and tools, together with the necessary further research on methods and tools. Throughout the lifetime of the project, the DEPLOY methods and tools will be intensively deployed in real industrial settings by the industrial partners in order to tension them against the industrial imperatives of cost-effectiveness, scaling and ability to cope with evolution of requirements. The industrial deployment will be in five sectors each of which is key to the future of European industry and society: automotive, rail transportation, space systems, business information and pervasive telecoms. These sector deployments will each be lead by a partner who are major players in their sector (Bosch, Siemens Transportation Systems, Space Systems Finland, SAP and Nokia respectively). The industrial deployment partners are committed to improving their development processes in order to meet the engineering demands of future systems.

DEPLOY will capitalise on the latest research from FP6 on formal engineering methods and tools along with related research on combining formal engineering methods with methods for resilience engineering. DEPLOY will deliver major new advances over these existing methods and tools. The technology-provider partners of DEPLOY have contributed to these existing FP6 results enabling the project to take advantage of their existing research and development base (Newcastle University, Aabo Akademi University, CETIC, ClearSy, ETH Zurich, Heinrich-Heine Universität Düsseldorf, Systerel and University of Southampton). The rich and complementary mix of expertise with engineering challenges from the industrial deployment partners together with the extensive technology base of the technology providers encompasses a consortium which is ideally suited to addressing the DEPLOY aims and which is unique in Europe and indeed internationally.

The experiences and requirements of the industrial deployment will continually feed back into the research and development of the DEPLOY methods and tools. The resulting DEPLOY methods and tools will be much more useful to a wider range of industry than earlier work from the formal methods community for the following reasons:

• They will support the rigorous engineering of complex resilient systems from high level requirements down to software implementations via specification, architecture and detailed designs.

• They will support thesystematic reuse and adaptation of models and software thus addressing industry’s requirement for high productivity and requirements evolution

• They will have been field-testedin, and adapted for, a range of industrial engineering processes

• They will be accompanied bydeployment strategies for a range of industrial sectors

• They will be based on an openplatform (Eclipse) that is already well-supported and used by industry, and will themselves be open

In order to achieve these results, the consortium has already identified further research issues that DEPLOY will need to pursue: on requirements validation and evolution, on reuse of models and software and on engineering for dependability including resilience, security and reliability; these are needed by industry but are not sufficiently well supported by current methods. This research will feed into the development of a powerful modelling, validation and verification toolset, based on Eclipse, that scales to problems of industrial size and is open to further extension and adaptation.

Dependability and Formal Engineering Methods

The consortium sees the problem of building dependable, well-architected and evolvable computer-based systems as crucial to the future of European industry at large and not just its IT industry. A system’s dependability is defined as its ability to deliver a service that can be trusted in a justifiable way[1]. To achieve the required level of dependability, systems must be engineered in such a way that they deal with both accidental and malicious faults that come from within the system or from the system environment. From its considerable experience of building large complex systems, the consortium has strong evidence that dependability can be achieved for such systems through the use of formal engineering methods that are grounded in mathematical modelling and analysis[2]. Modern formal methods support modelling and reasoning at multiple levels of abstraction enabling a systematic engineering flow from requirements specification, via architecture to detailed design and implementation. An engineering flow based on formal methods can exploit powerful automated validation and verification technology to ensure consistency between levels. Verification of consistency between abstraction levels, known as refinement, provides deep insight into and strong assurance of system dependability. A refinement-based approach enables mastery of system complexity through tractable abstract models of behaviour and architecture. Besides system dependability, the use of tractable models of architecture and behaviour also enables greater reuse and sound evolution of engineering effort. Reuse is important for increased productivity while design evolution is important for coping with changing system requirements. Furthermore, experience shows that deploying formal modelling and analysis early in the development life-cycle can reduce costs in the long run by reducing the expensive test and debug cycle and by providing more reliable services to users during system operation2.

Design for Resilience

To build trustworthy systems developers need to incorporate appropriate resilience mechanisms in their design in a systematic way to ensure that these systems continue providing the expected service in spite of various erroneous conditions in the systems and their environments. Complex modern applications constantly face a wide variety of such conditions (caused among others by malfunctioning infrastructures, environmental hazards, malicious intentions, software defects, degradation of services provided by components and component mismatches) that can have potentially damaging consequences if these mechanisms are not in place. Resilience is understood here as the requirement to be able to adapt to negative events and conditions (this term is used to cover several relevant concepts, such as fault tolerance and self-healing). ICT Challenge 1 of FP7 states that the future infrastructures will need to guarantee resilience compatible with software platforms reaching a complexity and scale that are an order magnitude greater than those of today's infrastructures. To be effective, resilience needs to be engineered in from the earliest stages of system design. The implication for DEPLOY is that our formal engineering methods must incorporate design for resilience at all stages. The success of the industrial deployment of advanced engineering methods will largely depend on their ability to enforce and support design for resilience. DEPLOY will combine formal methods and design for resilience in the engineering of dependable systems.

Coherent Large-Scale Integration of Deployment, Research and Development

Achieving deployment will involve a synergistic mix of scientific research, technology development and technology deployment. Deployment activities will be performed throughout the lifetime of the project and the needs and experiences of the deployment activities will drive the research and development activities. Technology development will be underpinned by scientific research and both will be validated through deployment. As well as playing the role of research and development drivers and validators, the deployment activities will also play the role of technology demonstrators in the later phases of the project. We will build organisational structures that ensure the results of DEPLOY are exploited beyond the lifetime of the project. Because of the range of activities involved, a synergistic mix of deployment, research and development can only be achieved in a coherent way as a large-scale integrating project (IP).

Five Sectors

Deployment will be in five sectors each of which is key to the future of European industry and society: automotive, rail transportation, space systems, business information and pervasive telecoms. It is essential for a project of this nature to cover a range of sectors as each of these sectors brings with them different needs. Each of the sector leaders in DEPLOY has already identified priority challenges in dependable systems engineering for their sector. These sector priorities complement each other to provide a broad coverage of engineering challenges. The initial phase of DEPLOY will involve intensive training for the industrial partners on state-of-the-art formal methods and tools. The training will be followed by a phase of pilot deployment on industrial products in each sector. The experiences of the pilot deployment will feed directly into the further advancement of methods and tools. These advances will then support the second phase of extensive deployment in each sector addressing production-level challenges. After each deployment there will be a phase involving rigorous evaluation of the industrial impact of the deployments along with the development of strategies for future deployment. The full workprogramme is described in Section B.1.3.

Success and Impact of DEPLOY

Methods, tools and ample experience exist to suggest that formal methods technology can bring significant benefits at affordable (and reducing) cost2. Industrial deployment of formal methods is not achieving its potential because many formal engineering tools do not scale well, do not deal well with requirements evolution and do not fit well with existing engineering practices for dependable systems. We will succeed in our deployment aims because we will focus on industrial deployment problems including dependability, scalability and evolvability, because we will conduct large simultaneous deployment in five major industrial sectors, because we will provide 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 will build on the existing successful Eclipse-based RODIN environment[3]. The core business of the industrial partners is the construction of safety-critical, business-critical and mission-critical systems. Such systems are required to have a high degree of dependability. The industrial partners know that achieving greater system dependability is essential to maintaining the competitive edge they currently enjoy through their excellence in engineering. 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 will address all these issues, helping the industrial partners to achieve real improvements in their engineering processes and, in the longer term, will lead to improvements in European industrial practice more generally.

Building on Existing FP6 Results

DEPLOY is timely because modern formal methods and tools are now reaching a degree of maturity and sophistication that allows them to be deployed on system development projects in industry. Seven of the DEPLOY partners are involved in the FP6 RODIN3 (Rigorous Open Development Environment for Complex Systems, 2004-2007) project which has already delivered an extensible open source platform, based on Eclipse, for refinement-based formal methods along with a body of work on formal methods for dependable systems. DEPLOY will exploit and build on these results. As is the case in RODIN, DEPLOY will use the Event-B formal method as a basis but will also explore extensions and other formal approaches where appropriate. The industrial deployment partners are ready and eager to exploit the results of RODIN and to contribute to the further research and development required to achieve industrial deployment of formal engineering methods. Besides RODIN, other relevant FP6 projects on which DEPLOY can build include MOBIUS, which is building an Eclipse-based toolset for validation of Java code, MODELPLEX, which is applying the semi-formal UML modelling notation to complex system design, SERENITY, which aims at providing security and dependability in Ambient Intelligence systems, and the ReSIST Network of Excellence on resilience for survivability.