ANR-10-SEGI-017

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

Accueil Projet CERCLES Partenaires Actualité Contact

This is an old revision of the document!


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.

cercles/accueil.1340662652.txt.gz · Last modified: 2012/06/26 00:17 by phil
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