PROGRAMME DE LA REUNION DU 31 JANVIER 2002
-------------------------------------------------------------------------
9H30 - 9H45 : Présentation de la journée
9H45 - 10H30 : "La normalisation dans le domaine nucléaire : la norme
générique 61508 ; la norme sectorielle 61513", Jean-Paul Bouard
(EDF/SEPTEN)
10H30 - 11H15 : "Validation d'un logiciel critique par retour
d'expérience selon la norme CEI 61508", Patrice Noury (Alstom
Technology), Michel Suzan (Bureau Veritas) [ppt]
11H15 - 11H30 : Pause
11H30 - 12H15 : "Vérification de spécification de logiciel critique",
Jean-Louis Boulanger [ppt]
12H15 - 13H30 : Pause déjeuner
13H30 - 14H15 : "CLAIRE, un environnement de test de systèmes
temps-réel distribués", Jacques Raguideau (CEA) [ppt]
Résumé. L'outil est présenté dans l'utilisation qu'en fait l'IPSN
pour émettre un avis technique à l'autorité de sûreté (DSIN) sur des
systèmes critiques tels que le système de protection des centrales
nucléaires françaises. Il s'agit de tester des systèmes comprenant
environ une dizaine de microprocesseurs, sans instrumenter le code
pour ne pas modifier le comportement temps-réel voire fonctionnel. La
solution est basée sur l'utilisation de simulateurs logiciels du
matériel dont les microprocesseurs. Elle permet l'observation fine de
l'exécution, et des essais qui seraient plus difficiles à faire sur
du matériel par exemple l'injection de fautes.
14H15 - 15H00 : "Caveat, un outil d'analyse statique et preuve de
programmes C", Jacques Raguideau (CEA) [ppt]
Résumé. L'outil est utilisé par EDF pour répondre rapidement aux
questions formulées par l'IPSN sur des systèmes critiques développés
hors EDF. Il permet de montrer que des situations indésirables comme
une division par zéro, une portion de code inaccessible, etc.,
n'existent pas étant données certaines hypothèses sur l'environnement.
Il est aussi utilisé par Airbus France dans le développement en C des
parties les plus critiques de l'A380. Il s'agit là de prouver les
fonctions dès qu'elles sont écrites de façon à ne pas attendre les
phases de test pour trouver des erreurs. L'objectif est donc plus la
réduction des coûts et délais que la preuve pour elle-même.
15H00 - 15H15 : Pause
15H15 - 16H00 : "Analyse de codes critiques par analyse statique :
expérience d'EdF", Alain Ourghanlian (EdF, R&D) [ppt]
Résumé. En tant qu'exploitant de tranche nucléaire, EDF est
responsable de la qualification des systèmes numériques programmés
mis en exploitation.
Les fonctions supportées par ces systèmes ainsi que leur coût de
développement prend une part de plus en plus importante sur les sites
nucléaires. Afin d'optimiser le coût de qualification de ces
systèmes, EdF a lancé un projet de recherche et développement. Une
des actions de ce projet est d'analyser l'apport des outils d'analyse
de la sémantique des codes, récemment apparus sur le marché, pour
contribuer à qualifier ces systèmes programmés.
Une première expérimentation a été menée sur des logiciels classés de
sûreté. L'outil Polyspace C Verifier, de PolySpace Technologie, ainsi
que l'outil CAVEAT, développé au CEA Saclay, ont été utilisés. Ces
logiciels classés de sûreté sont caractérisés par un volume de code
réduit, des fonctionnalités simples, une architecture simple (boucle
séquentielle) et la disposition de l'ensemble du code source. Cette
première étude concluante, nous a permis d'étendre l'utilisation de
ces approches sur des logiciels moins critiques, mais plus complexes.
16H00 - 16H45 : "Methode de communication entre specifieurs (Systemes et
Logiciels)", Société SURLOG. [zip]
16H45 - 17H00 : Conclusion de la journée. Informations sur la SEE et
la vie du Club (notamment, renouvellement de quelques animateurs des
Cercles).