About Deploy Project
Workpackage 3 — Deployment in the space sector
Development of safety critical software in the space sector aims at producing high quality software that ensures the safety
of human lives, achieves mission objectives, and correctly operates valuable instruments. The big challenges in space projects
are tracing requirements to the different levels of specifications, validating that requirements have been implemented, and making
sure that reliability and safety aspects have been properly taken into account. The development process in the space sector is
controlled by existing standards and regulations that must be followed by suppliers of software to space
projects (e,g. the Software Engineering Standard by the European Consortium for Space Standardization ECSS-E-40B).
SSF will lead a workpackage that aims at deploying and integrating refinement-based methods and tools into existing development
processes for space applications. An important goal of the workpackage is to develop a methodology for increasing the level of automation
in the development process while maintaining compliance with existing standards and regulations. A higher level of automation can help
to sustain the productivity and competitiveness of the European space sector.
Description of Work.
The workpackage has been split into seen tasks that are described below. The goals will be achieved by successively introducing
new methods into SSF’s BepiColombo project. BepiColombo is a European Space Agency (ESA) mission that will explore Mercury, the planet
closest to the sun. Studying Mercury will provide scientist with understanding how planets form. SSF is in charge of the design and
development of on-board software for the X-ray instruments on board ESA’s BepiColombo spacecraft. The planned launch date for BepiColombo
is in August 2013. The length of the BepiColombo project provides a firm foundation to build the integration process on.
Tasks T3.1-T3.2 on Technology Transfer: The goal of the first two tasks is to familiarise engineers and managers with the
Event-B and the available tools, and also identify potential problems in applying the new methods. We also aim at identifying methodological
and tooling challenges from the space sector to feed them into research and development activities of WP6-WP10.
Tasks T3.3-T3.5 on Deployment: Deployment is split into the two main phases. In the first phase of the deployment we reformulate
selected parts of the requirements document for the Telemetry/Telecommand software (TM/TC software) used in BepiColombo, so that it could
be used as a baseline for formal modelling. A formal model of the software will be constructed. A specific focus will be on investigating
how requirements tracing and validation can be accomplished, as these are prime concerns for contractors in the space sector. We investigate
how resilience and safety can be addressed in the development process. Refinement proofs ensure that once a requirement has been correctly
modelled, successive models will also implement the requirement. However, since requirements can be erroneously modelled or completely missed
other techniques are also required. We will also assess which parts of the on-board software will be the primary targets for the enhanced
deployment. During the enhanced deployment the TM/TC software will be subjected to more deep deployment of the formal engineering methods.
We will investigate integration with the RAMS (reliability, availability, maintainability, safety) activities and potentials of reuse for
Tasks T3.6-T3.7 on Method Assessment and Integration: The cost-effectiveness and benefits of using formal models will be measured
and evaluated. Moreover, we will investigate how to integrate proposed methods and tools into the existing development practice.
Expected Results. The WP will deploy advanced methods and tools for automatic refinement-based verification and validation
and integrate them into the existing development processes for space applications. The methods will facilitate reuse, provide support
in requirements evolution and software design as well as increase the reliability and productivity.