About Deploy Project
Methodological research and development Workpackages : WP6-WP8
These workpackages address research issues that have been (or will be) identified, by the industrial partners,
in the deployment of formal methods for engineering of dependable systems. The activities of these workpackages will
be a mixture of:
- Scientific research providing conceptual extensions of the foundations of our methods
- Development of methodological guidelines on the practical application of the methods
- Research that makes the development of powerful new tool support possible
The results of WP6-WP8 will normally feed into WP9 as tool requirements/definitions and/or into WP1-WP4
in the form of deployment guidelines. Tool developments from WP9 will in turn be field-tested in WP1-WP4.
We are quite clear that the breadth of application areas in DEPLOY will give rise to questions that will
require new ideas; this will be an evolving picture reflecting the changing needs of the industrial deployments.
As set out in Section B.2.1, the DEPLOY Project Board will oversee the project re-focus point at M19 that will
help us to revise our research priorities.
What we present here is our initial set of research priorities whose study can be foreseen as important
– this judgement is based on our previous experience with the application of such methods and intense discussion within
the consortium during the proposal preparation stage.
The initial methodological areas where advances are required are in 1) supporting requirements validation and evolution,
2) enhancing productivity through reuse and 3) formal arguments about dependability. Thus the work on methodological research
and development is organised into three work packages focussing on requirements, reuse and dependability. We have identified
priority objectives for each of these work packages. At the re-focus point in M19, we will revise the objectives of each work
package based on experiences of the industrial deployment in WP1-WP4. If necessary we will create new work package structures at M20.
WP6 Requirements Validation and Evolution:
Informal requirements documents typically present requirements in terms of disparate levels of abstraction; some will be
very high-level user-oriented requirements while others will be described in terms of very detailed design- and implementation-oriented
thinking. Our experience is that, prior to any formal modelling, it is important to structure informal requirements into small
identifiable chunks and categorise them according to feature and abstraction level. This facilitates tracing of requirements
through the different abstraction levels of a refinement-based formal development. Further research and development is required
to provide techniques that enable systematic validation of requirements throughout the development cycle. In addition, since
requirements change in response to market pressure and in response to increased understanding of a domain during development,
it is essential to support effective evolution of formal developments to reflect evolution of requirements. The priority objectives
identified for WP6 are to
- investigate advanced techniques for managing and validating requirements for complex dependable systems
- create techniques for tracing requirements throughout entire formal development process from abstract specification to implementation
- develop approaches supporting requirements evolution in the formal system development
- enhance techniques for integrating requirements obtained from RAMS (reliability, availability, maintainability, safety)
activities into formal system modelling and analysis
This work is initially structured into two tasks: T6.1 on requirements tracing and validation and T6.2 on Requirements evolution.
T6.1 will develop techniques for tracing requirements throughout the entire formal development process. T62 will focus on the techniques
for efficient capturing new and altered requirements.
WP7 Productivity through Reuse
Reuse of all forms of intellectual artefacts involved in development is essential to achieve the increased levels of
productivity at which DEPLOY aims. Such artefacts can include specifications, designs, refinement patterns, formal analysis,
software components and software product families. This WP will provide methodological advances to support reuse of models,
reuse of refinement and design patterns and reuse of formal analysis. Formal modelling is key to achieving the right
abstractions required to identify the ways in which components can be reused. Along with abstraction, composition and
decomposition are key enablers of reuse of models and associated analysis. This is because it is more feasible to reuse
components and subsystems rather than complete systems. A particular interest will be to ensure our methods cover the sort
of generic (instantiatable) system that is so clearly embodied in SAP products. The priority objectives identified for WP7 are to
- develop the advanced techniques for composing and decomposing formal models and proofs (task T7.1)
- investigate techniques for formal representation of design patterns and associated techniques for construction,
instantiation and composition of formal design patterns (task T7.2)
This work is structured as two tasks: T7.1 on composition and T7.2 on design patterns. T7.1 will develop and support general mechanisms
to enable the construction and compositional deployment of reusable artefacts.T6.2 will develop a language to represent patterns formally
and a tool that support construction, instantiation and composition of patterns.
WP8 Achieving and Demonstrating Dependability
Systems that operate in hazardous environments must maintain dependability even though they contain (often physical)
components that may fail. The abstraction and precision afforded by formal modelling and analysis are essential to mastering
the complexity inherent in the threats to system dependability and the mechanisms engineered in to tackle those threats.
Formal models and analysis also provide valuable evidence for providing high levels of assurance of system dependability.
Priority objectives of WP8 will be to
- develop advanced modelling techniques supporting development of dependable systems including stochastic requirements
- ensure system resilience, security, reliability and safety by effective and systematic integration of the appropriate
measures into the entire development process starting from abstract system models (tasks T8.2-T8.4)
- develop further techniques for deriving system specifications from a description of their environment – this will
include fault assumptions about their environment (task T8.1)
- develop a set of modelling and analysis patterns supporting the correct application of advanced dependability
mechanisms during system development (task T8.2).
This work is structured as four tasks: T8.1 on specifying fault tolerance, T8.2 on resilience, T8.3 on security and T8.4
on stochastic reasoning. T8.1 will focus on obtaining specifications of resilient systems. T8.2 will develop methods and
models ensuring effective and systematic integration of resilience into system design. T8.3 will deal with use of modelling
and refinement in developing correct secure systems. T8.4 will develop techniques for reasoning about probabilities of hazardous