Rechercher dans les archives
Retour aux sommaires
Approche synchrone et logiciels critiques pour l’automatique
Mois: 01
Année: 1995
Numéro : 1/1995
DOI: 10.3845/ree.1995.012
Première page: 71
Dernière page: 78
Type: Dossier
Thème: Génie logiciel
Titre: Approche synchrone et logiciels critiques pour l'automatique
Nom de l'auteur: DUBOIS
Prénom: Christian
Affiliation: Schneider Electric, Département SES
Mot-clé: Génie logiciel
Mot-clé: Nucléaire
Mot-clé: Langages synchrones
Mot-clé: Vérification formelle
Introduction: Le contrôle-commande d'une centrale nucléaire constitue un domaine d'application critique pour les logiciels. Schneider Electric a choisi un atelier graphique de développement basé sur un langage à flot de données synchrone. Ce type de langage, proche des habitudes de programmation des automaticiens, permet la verification formelle de propriétés de programmes.
Résumé: L'atelier SAGA basé sur un langage à flot de données synchrone, LUSTRE a été choisi pour le développement du contrôle commande du SPIN (Système de protection intégré numérique) N4 des centrales nucléaires 1 450 MW. Dans un langage synchrone, les variables sont des fonctions du temps, le temps étant discret. Le formalisme rigoureux de LUSTRE est bien adapté aux applications dans le domaine de l'automatique. L'atelier SAGA entièrement basé sur LUSTRE est cependant ouvert sur le code C. Il assure des vérifications de cohérence tout au long de la programmation. Une méthode de vérification formelle de propriétés (de sûreté) a par ailleurs été développée à partir de SAGA et de LUSTRE et a donné naissance à l'outil LESAR.
 au compte de lecture pour accéder au document