Context
Safety critical systems, i.e. systems with the potential to endanger a person’s life, are often subject to a certification process. In that case, a certification authority assesses the overall conditions of design and the compliance of the product with the regulatory requirements. When the authorities are positively convinced, they deliver a certificate that authorizes its operation.
Figure above highlights the main idea behind the certification activities in the aeronautics domain: expert committees, composed of independent associations, companies, certification authorities, and academics have written several standards 1 in order to answer the regulation laws. Those documents have been recognized and validated as Acceptable Means of Compliance (AMC) [EAS19]. Thus, any applicant requesting the certification of a system is in charge of proving that their product is compliant with the standards. For multi-core-based systems, the Multi-Core Certification Review Item (MCP-CRI) (also known as the CAST-32A position paper [Cer16]) provides a set of guidances for software planning and verification on
multi-core chips.
To convince a certification authority, applicants must provide all elements pertaining to the design of the system and to the Verification and Validation (V&V) operations that have been carried out. All of these elements are generally referred to as an assurance case. An assurance case can be defined as “an organized argument that a system is acceptable for its intended use with respect to specified concerns (such as safety, security, correctness)” [RKR15]. Thus, not only must the applicant provide a certain number of elements, but they must also argue why these are sufficient to cover the high level objectives defined by the standards.
PHYLOG aims at preparing certification activities related to multi-core-based systems. In particular, the purpose is to provide a framework that allows any applicant to prepare their certification documentation.
Project objectives
To reach this general objective, we have defined a certification framework based on:
- justification patterns to express any argumentation. The idea is to organize any argumentation around structured graphical notations diagrams. More precisely justification patterns are templates specifically dedicated to expressing a structured reasoning with a set of evidences. We have translated most of CAST-32A objectives as generic justification patterns. The basics of the approach were defined for the certification of IMA systems in [BBD+16, Pol16]. The generic justification patterns for the CAST-32A are described in the Patterns;
- and formal and automatic analyses to support the proof of the argumentation. A justification pattern comes with a series of evidences that support the reasoning. Among those evidences, two types of analysis are required by the MCP-CRI: interference analysis and safety analysis. Because of the large size of multi-core platforms and their complexity, those analyses can lead to combinatorial explosion and some misinterpretation. We have defined a topological interference analysis and a preliminary safety assessment analysis.