CERtification Compositionnelle des Logiciels Embarqués critiques et Sûrs (CERCLES)

L’Agence Nationale pour la recherche a retenu le projet de recherche industrielle CERCLES (Certification compositionnelle des logiciels embarqués critiques et sûrs), dans le cadre de l’édition 2010 du programme ARPEGE.

• DURÉE : 36 mois
• PARTENAIRES : SAGEM (Leader)

Partenaires

• CLEARSY
• Le laboratoire PPS (Preuves Programmes et Systèmes – Université Paris Diderot)
• Le laboratoire LIP6

Cadre

Le projet CERCLES concerne la certification des logiciels embarqués critiques et sûrs, le but étant 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é. L’idée pour tenter de diminuer son coût – et qui fait l’objet de cette proposition – est de capitaliser la certification des composants par l’intermédiaire de composants pré-certifiés. 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 permettront de construire l’architecture du système final en induisant sa certification. Des démarches similaires existent dans le cadre du développement des langages de programmation mais elles n’abordent pas le domaine du logiciel critique embarqué pour lequel l’exigence de certification est un préalable incontournable.

Schématiquement, si A et B sont des composants pré-certifiés alors on veut disposer d’un moyen permettant 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 » offrant certaines garanties de fonctionnement et possibilité d’assemblage. Sur cette base, on peut espérer établir à la fois la préservation de la correction des composants assemblés et la correction de l’assemblage par rapport à ses propres exigences. En particulier, on pourra vérifier que les propriétés émergentes d’un assemblage sont ou bien celles attendues 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 pour le besoin de la certification. En particulier, comment, à partir des tests associés à chaque composant, créer une batterie de tests globaux montrant que les assemblages réalisés respectent 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.

Avancée scientifique attendue

Les principaux résultats attendus sont :

• La fusion de plusieurs modèles formels. Etant donnés n modèles caractérisant chacun un composant, trouver un opérateur de fusion tel que « l’addition » de ces n modèles représente le modèle d’un composant « somme ». Ainsi la « somme » de plusieurs composants (au sens de CERCLES) sera également un composant de même nature.
• La cohérence des modèles. Démontrer qu’un ou plusieurs modèles locaux Mi sont logiquement cohérents avec un modèle plus général de plus haut niveau M. Autrement dit que M ⇒ Mi. L’idée (compatible avec la démarche de l’Atelier B) est de procéder par raffinements successifs de M afin de retrouver chaque Mi. En effet, il faut un procédé adéquat permettant de réduire l’écart entre le niveau de M et celui des Mi.