The “Agence Nationale pour la Recherche”( *-National Research Agency) has retained the industrial research project CERCLES (Compositional certification of critical and safe embedded software) within the scope of the ARPEGE programme for 2010. This 36-month project includes the following partners:
- SAGEM (leader)
- The PPS laboratory (Proof Programmes and Systems – Paris Diderot University)
- The LIP6 laboratory
This project is supported by System@tic .
The CERCLES project entails the certification of critical and secure embedded software, thus aiming to considerably reduce the costs of the process . Software certification for critical embedded systems is a very difficult and tedious industrial operation. It must adhere to a long, rigorous and extremely standardised process. The attempt to reduce these costs, thereby forming the basis of this proposal,is to economize the certification of components through pre-certified components. As a result, the problem faced relates to the availability of fairly inexpensive assembly methods and tools which can be industrialised,thereby enabling the architecture for system to be finalised leading to its certification. Similar procedures exist within the scope of programming language development but they don’t tackle the domain of critical embedded software, for which the need for preliminary certification is essential.
Schematically, if A and B are pre-certified components then we want to have an available means of enabling assembly of A and B to be tested. Among other things, this will require knowing how to correctly describe units A and B as “components”, providing certain guarantees as to their operation and eventual assembly. On the basis of this, hopefully, it may be possible to establish a safeguard for the corrective measures to assembled components and for assembly in relation to its own requirements. In particular, we would like to verify that the emerging quality characteristics of an assembly are either those expected or those which don’t interrupt the functionality of the system in its operational context.
In more concrete terms, we’d say that the aim of the CERCLES project is to resolve the issue of intergrating testing to meet certification requirements. Of particular interest is how, from the tests associated with each component, to create a battery of global tests indicating if the assembly performance complies with the system’s requirements. The anticipated automation of this test creation process will lead to a reduction in the costs associated with assembly certification.
Expected scientific progress
The main results expected are:
- The consolidation of several formal models. Given that the n-models each characterise a component, finding a method of consolidation such as “the addition” of these n-models, represents the model of a “sum” component. In this way the “sum” of several components (within the meaning of CERCLES) will also be a component of the same nature.
- The consistency of models. To demonstrate that one or several local Mi-models are logically consistent with a more general and higher level M-model. In other words M ⇒ Mi. The idea (compatible with the Atelier B approach) is to proceed with successive refinements of M in order to find each Mi. In fact, you need a suitable process enabling the distance between the level of M and that of Mi to be reduced.