IMA Separation Kernel Qualification - preparation
| IMA Separation Kernel Qualification - preparation | |||
| Programme: | GSTP | Achieved TRL: | 4 |
| Reference: | G607-29SW | Closure: | 2016 |
| Contractor(s): | SciSys (GB), Airbus DS (FR), Thales Alenia Space (FR), LERO (IE) | ||
In order to address the increasing complexity of spacecraft avionics, ESA have explored technological solutions adopted by the aviation domain for this purpose: Integrated Modular Avionics – IMA, and time and space partitioning – TSP.
The functional content of spacecraft is increasing and with this the complexity of the subsystems implementing the functions. This has been addressed by using an increasingly federated avionics architecture where each function has its own node in the avionics platform. However, this leads to increasingly complex interactions between different subsystems, as well as increased requirements on mass, volume and power. One major advantage of the federated approach to avionics is the inherent separation of different applications and functions, providing, for instance,
a) natural non-interference between different software applications, both for the fault free case and when faults are present,
b) physical fault containment regions limiting any propagation, and
ability to verify and validate software applications in parallel, largely independent of each other. The IMA-SP platform is dedicated to supporting the time and space partitioning of the spacecraft applications. The core software component is called the System Executive Platform software (SEP). The SEP contains a kernel that schedules the execution of partitions and provides the partitioning mechanisms. Inside a partition a local scheduler (guest OS) may be used to execute concurrently several independent processes.
Achievements
One of the goals of the study is to establish a requirement baseline for the use of Partitioning kernels in space from the different existing standards. It started from the well-known ARINC 653 standard that is used in aeronautics to design IMA (Integrated Modular Avionics) and the tailoring done during a previous ESA study, IMA for Space (IMA-SP). The System Software Specification from LVCUGEN that was written by CNES and that is based on the partitioning kernel Xtratum has also been used as a reference for space utilisation of partitioning.
The requirements have been divided in different categories:
- CORE Requirement. A CORE requirement is a requirement specifying an essential functionality of the partitioning kernel under specification.
- EXTENDED Requirement. An EXTENDED requirement is a requirement specifying a non-essential or highly specific functionality of the partitioning kernel under specification. These requirements are second priority requirements that can be de scoped in a qualification process. According to this semantics, the requirements baseline for the qualification process can be tailored according to specific needs. A tailored requirement baseline shall at least contain all CORE requirements.
The picture on the right explains the use of Jitters for MAF synchronization. In the normal case the synchronization signal is raised in the time interval (T;T+Jitter). The next occurrence of the MAF is started on reception of the synchronization signal.
If the synchronization signal is received before the completion of the MAF (Case 2), a synchronization error is detected by the partitioning kernel. In this case, the partitioning kernel starts the new occurrence of the MAF at the end of the previous one and sends a synchronization error indication to the health monitoring which has to apply the action related to this synchronization error. A common usage is to propagate the synchronization error to an authorized partition, which implements the FDIR strategy.
If the synchronization signal is not received at the time T+Jitter (Case 3) then the partitioning kernel should start the new occurrence of the MAF and send a synchronization error to the health monitoring.
The picture to the left gives an overview of the development and qualification activities. The qualification process takes place after the development activities and after the qualification preparation activities. Those activities are depicted on the figure. Some of these activities have been realized during the IMA Kernel Qualification Preparation study:
This first evaluation allows identifying of the distance between the PK quality and the target quality level. This drives the decision to make additional PK evolutions (in code or documentation) in order to reach the expected quality level, or simply increase it. This corresponds to the SPEC activity "definition of corrective actions".
Decided corrective actions are performed, and qualification artefacts are updated to allow a second evaluation. This corresponds to the "SPEC Re-evaluation of the implementation of the proposed corrective actions phase". Qualification succeeds when the acceptance criteria is fulfilled.
The study has written a requirement baseline for the use of Partitioning kernels in the European space domain. It is based on the well-known ARINC 653 standard that is used in aeronautics to design IMA and includes user needs identified in previous ESA studies (IMA for Space) and the System Software Specification from LVCUGEN. As well as requirements for single core processors, the requirement baseline also addresses multicore processors because they are seen as important targets for the future.
Following the definition of the Requirement Baseline, the Qualification Strategy and Plan was defined. This document defines the qualification process with the different activities, the roles, and the responsibilities, to achieve the qualification credits for a Partitioning Kernel on a particular target board.
To handle software complexity, and reduce the costs and planning of the V&V activities of one or more Partitioning Kernels, the objective was to select the best-suited techniques to assess Partitioning Kernels against the quality model, and to verify and validate the requirements, depending on their nature.
As part of the qualification, planning and investigation was performed of the best-suited techniques to handle software complexity and reduce the costs of assessing Partitioning Kernels against the quality model and to verify and validate the requirements. The classical methods and techniques, as well as two alternatives, Formal Methods and Model Based Testing, were investigated.
The Validation test plan describes a generic test system and set of tests to validate any partitioning kernel against the specified requirements, the partitioning kernel baseline requirements. The test cases were mostly classical techniques with a subset of them using Model Based Testing.
All core and extended requirements applicable to ‘single core’ systems are validated by the test plan. For a small number of requirements which are not fully testable, or a test does not provide sufficient validation, the requirement is verified by analysis, inspection or review. Dependability and robustness test are also included in the test plan.
The validation environment was prepared for the classical tests and all the necessary test artefacts defined. The classical test environment allows the full automation of the tests and is designed to be easily portable been different target boards and host computers. The test environment allows low level access to the hardware to validate the implementation of the requirements.
MBT techniques were demonstrated by a documenting a theoretical analysis, due to the non-existence of appropriate tooling, experimentation activities related to MBT in the case study were not possible.
A bottom-up approach using the Frama-C tool and the ACSL language was experimented on a small set of Xtratum functions, which gave some interesting results.
The case study has demonstrated the majority of the test techniques for classical tests and these techniques have been shown to work. The test techniques are feasible and appropriate for the validation of a PK. The testing has been sufficient to identify anomalies in the Xtratum implementation.And so on.
Further work
This study is the preparation for the full Partitioning Kernel Qualification, preparing activities to qualify Xtratum, PikeOs, and possibly AIR. This qualification will be performed following the qualification strategy defined in this study, and will consider the requirement baseline and the test plan. This qualification will involve the development of the qualification test suite.
Model Based Testing could be explored further in the context of the On-board software Reference Architecture.