ANR-10-SEGI-017

La Certification Compositionnelle des Logiciels Embarqués CritiqueS et Sûrs

Accueil Projet CERCLES Partenaires Actualité Contact

La Certification Compositionnelle des Logiciels Embarqués CritiqueS et Sûrs

Le projet CERCLES est centré sur la certification des logiciels embarqués critiques et sûrs. Le but est de diminuer notablement le coût de cette opération.

La certification des logiciels des systèmes embarqués critiques est une opération industrielle très difficile et fastidieuse. Elle doit respecter un processus long, rigoureux et extrêmement normé. Par exemple la norme DO178B de l'aviation civile, décrit l'ensemble des processus de spécification, conception, codage et vérification du logiciel qu'il faut satisfaire pour obtenir la certification. Le développement logiciel moderne repose sur la mise en oeuvre de composants et de leur assemblage. La norme de certification, en particulier dans son exigence de vérification reposant sur des tests, conduit concrètement à avoir à suivre deux fois le même chemin: une fois lors du développement des composants et une seconde fois lors de leur assemblage. Ce qui induit un coût. L'idée pour tenter de diminuer ce coût - et qui fait l'objet de cette proposition - est de capitaliser la certification des composants. En conséquence, le problème à résoudre est celui de l'existence de méthodes et outils d'assemblages peu coûteux et industrialisables qui permettent de construire l'architecture du système final en induisant sa certification.

De telles voies ont déjà été explorées dans le cadre du développement des langages de programmation (typage, objets, modules, contrats) proposant des modèles originaux de conception ou de codage. Mais elles n'abordent pas le domaine du logiciel critique embarqué pour lequel l'exigence de certification est un préalable incontournable (normes de certification) et en particulier, l'exigence de vérification reposant sur des tests et leur analyse de couverture. Il faut obtenir que si A et B sont des composants préalablement certifiés alors on dispose du moyen de vérifier l'assemblage A-B. Ceci imposera, entre autres, qu'on sache décrire correctement

  • les unités A et B en tant que «composants» (par opposition à une application complète) offrant certaines garanties de fonctionnement et possibilité d'assemblage;
  • la composition A-B en tant qu'assemblage préservant les garanties établies pour ses composants et réalisant d'autres exigences de fonctionnement.

Sur cette base, on peut espérer établir et la préservation de la correction des composants assemblés et la correction de l'assemblage par rapport à ses propres exigences. En particulier, que les propriétés émergentes d'un assemblage sont ou bien celles attendue ou bien telles qu'elles ne nuisent pas au fonctionnement du système dans son contexte opérationnel. Plus concrètement, nous dirions que le but du projet CERCLES est de résoudre le problème de l'intégration de tests. C'est-à-dire, comment, à partir des tests associés à chaque composant, créer une batterie de tests globaux montrant que l'assemblage réalisé respecte les exigences du système. L'automatisation escomptée de cette création de tests induira une réduction du coût de la certification de l'assemblage.


The CERCLES project is focused on the certification of safety critical embeded software. Its aim is to reduce the cost of this activity.

The certification of safety critical embeded software is a costly industrial process. It has to follow a very long, rigourous and standardized process. For instance the DO178C standard of civil avionics describes the set of spécification (High Level Requirements), design (Architecture and Low Level Requirements), coding and verification activities that must be fulfilled to obtain the certification.

The modern software development relies on assembling components. In such a case, the certification standard, in particular as testing is required in the verification activity, leads to cover twice the same way: a first time during the development process of the components and a second time when the coponents are reused in another system.

The broad thrust of the CERCLES project is to capilalize on components certification in order to avoid the cost of covering twice the same way. The problemn is then the existence of methods trustful and tools for assembling components that are suitable for industry and capable to design system's architectures involving their certification.

Programming languages have still proposed methods and tools (typing, objects, modules, contracts) to increase the safety of reusing software components. But they did not address the specific point of safety critical embeded software for which a verification activity that relies on testing (and its coverage measurement) is absolutly required. We must obtain that if two components A and B have been previously certified then we have a way to verify the assembly A-B. This entails that we are able to describe faithfully

  • the units A and B as “components” offering some guaranted functionnal properties and some possibilty of reuse;
  • the composition A-B as an assembly preserving the guaranties acquired by the components and realizing some other specified functionalities.

On this basis we can expect to be abble to set both the preservation of correctness of the reused components individualy and the correctness of the composition with regards to its own requirements.

cercles/accueil.txt · Last modified: 2014/04/30 15:07 by pascal
Cette page utilise JavaScript. Si ce texte est visible, c'est que JavaScript est indisponible. Certains contenus ne vous sont alors pas accessibles.
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki