Plate-forme Systèmes et Logiciels Critiques

Autofor

Plan

gorigh.gifPrésentation

gorigh.gifButs et moyens

gorigh.gifJSLC 2000

gorigh.gifJSLC 2001

gorigh.gifProjets-pilote

gorigh.gifClub des Partenaires

gorigh.gifNous contacter

gorigh.gifLiens


Plate-Forme ``Systèmes et Logiciels Critiques''

Plate-Forme ``Systèmes et Logiciels Critiques''

Projet AUTOFOR

Méthodes Formelles pour les Automatismes de Sécurité

Rapport d'avancement 2000

(Version provisoire au 17/11)

 

TELECHARGER LA DEMO

Il s'agit d'une demo pour PC (Window 95 et +) et Mac.
Le fichier de 24 Mo est un ensemble de fichiers autodécompactable. Sauvegardez ce fichier dans un répertoire puis cliquer sur son nom pour le décompacter et l'installer.

 

DESCRIPTION DU PROJET

Résumé

Le projet a pour objectif de définir un environnement de spécification, de conception et de validation d'automatismes critiques. Il s'intéresse aux aspects suivants :

  • La sûreté des applications logicielles : notre objectif est de développer un environnement permettant d'apporter une "confiance justifiée" dans le système programmé dans son ensemble.
  • La sûreté des moyens de communication : notre objectif est de construire des "best practices" et de proposer des solutions favorisant la mise en oeuvre de réseaux de communications dans un contexte de sûreté.
  • Le lien avec la sûreté des procédés : notre objectif est d'élargir le champ d'application des méthodes formelles et de les rendre accessibles à l'utilisateur, à partir d'une représentation qui lui est familière.
  • Satisfaire les contraintes normatives, de certification : le projet AUTOFOR vise à apporter des réponses pratiques aux besoins de validations : donner des éléments méthodologiques cohérents avec les normes applicables et à les faire partager avec les acteurs français ou internationaux concernés (INERIS, INRS, IPSN, TÜV, COFRAC, etc.).

Etat de l'art

Développé par la société Télélogic, en étroite collaboration avec Schneider-Electric et Aérospatiale, SCADE est un atelier de programmation de systèmes réactifs, fondé sur le langage synchrone LUSTRE, défini au laboratoire Vérimag. Vérimag a développé l'outil LESAR de vérification de propriétés de sûreté des programmes LUSTRE. Les outils LUTESS et LURETTE, élaborés respectivement aux laboratoires LSR et Vérimag, permettent de produire automatiquement des séquences de test conformes à une spécification de l'environnement d'un programme LUSTRE.

En ce qui concerne les "briques matérielles" qui sont support du projet, on peut noter :

  • le réseau de communication NERVIA : développé par Schneider Electric pour ses applications dans le domaine du nucléaire, NERVIA est un réseau de communication qui présente des caractéristiques de sûreté élevées.
  • l'automate QUANTUM : appartenant a la gamme des automates Schneider (Momentum, Premium, ...), l'automate Quantum est le plus puissant. De plus, il possède des fonctionnalités (e.g. "hot standby"), qui permettent de l'intégrer dans des architectures de sûreté.

 

 

Situation du marché, analyse de la concurrence

Les offres industrielles actuelles sont basées sur des approches "standard ", elles s'appuient sur l'utilisation de redondances, logiques à pannes orientées, autotests, etc. Généralement, elles n'apportent pas de garanties formelles sur le développement des applications logicielles et sur la prise en compte des risques du procédé. Mais de plus en plus, les industriels cherchent des solutions "standard" plus performantes en terme de qualité du logiciel. Ce besoin est lié à l'émergence de nouvelles normes (CEI 61508, GAMP) et à des impératifs de productivité et de disponibilité des installations. L'offre française dans le domaine de l'automatisme de sécurité industriel est faible, alors que dans des secteurs spécifiques où l'on utilise une approche "contrôle-commande" (e.g. énergie, transport aérien), nous avons des solutions innovantes et efficaces (e.g. les outils basés sur Lustre). AUTOFOR vise à favoriser une rupture technologique, tirant parti de nos réalisations afin de proposer les services (validation d'applications), les briques de base (réseaux de sûreté) et la démonstration de la sûreté de nos solutions techniques (certification).

Cette démarche de rapprochement entre les acteurs du contrôle-commande traditionnel et les fabricants d'automates de sécurité est générale au domaine des automatismes. On peut noter : MOORE racheté par Siemens, partenariats entre HIMA et différents systèmes-intégrateurs (e.g. Schneider Electric), TRICONEX racheté par INVENSYS, PEPERL&FUCHS racheté par HONEYWELL,... Il est clair que nos concurrents visent à tirer le meilleur parti de ces deux types de solutions pour accroître leur présence sur le marché des automatismes.

Notre offre basé sur le langage formel Lustre constitue une différenciation concurrentielle importante : éprouvé dans le domaine du contrôle-commande nucléaire et de l'avionique, elle est un facteur important de notre extension sur le marché des automatismes.

INTERÊT DU PROJET

Description scientifique

L'objectif général du projet AUTOFOR est le développement de méthodes de conception d'automatismes de sûreté. Les méthodes envisagées s'articulent sur plusieurs axes:

  • L'utilisation et l'extension de l'atelier SCADE et des outils de validation formelle associés, pour la conception de logiciel pour automates programmables. Dans ce domaine, les objectifs d'AUTOFOR sont
    • de permettre la programmation d'automates programmables, et leur validation, à l'aide de SCADE
    • d'offrir, en amont de SCADE, des formalismes standard aux utilisateurs d'automates (Grafcet, matrices cause-effet, ...)
    • d'unifier et de compléter les outils de test LUTESS et LURETTE
    • de concevoir un outil d'aide au débogage de programmes

  • La mise en oeuvre, dans de tels logiciels, de méthodes d'évaluation et de renforcement de la sûreté de fonctionnement des automatismes.
  • Le renforcement de la sûreté des communications, dans le cas d'implantations distribuées.

 

 

Pertinence du projet par rapport au marché

Le marché des automatismes de sûreté est un marché en forte croissance. On peut noter quelques chiffres :

  • 2,2 milliards de francs aujourd'hui
  • 10% de croissance par an sur les 5 ans à venir
  • 3,6 milliards de francs en 2003.

Plusieurs constructeurs jusque là tournés vers des applications ciblées s'affrontent sur ce marché en pleine expansion : les constructeurs de contrôle-commande, les constructeurs d'automates standard, les constructeurs d'automates de sécurité.

AUTOFOR s'inscrit dans la stratégie de Schneider d'aborder ce marché.

 

Partenaires

  • Université Joseph Fourier - Laboratoires VERIMAG et LSR.

Le laboratoire VERIMAG développe le langage Lustre qui constitue le socle du projet, ainsi que les outils associés de vérification formelle Lesar et de génération de test Lurette. VERIMAG entretient depuis longtemps une collaboration scientifique et technique avec Schneider-Electric. Le laboratoire LSR construit l'outil Lutess, également dédié au test des programmes Lustre.

  • Schneider Electric, groupe mondial, a pour métiers de base la maîtrise de l'énergie électrique et les automatismes industriels. De ce fait, Schneider Electric développe et met en oeuvre des systèmes de contrôle-commande et des automates programmables. En particulier, Schneider Electric réalise des systèmes de contrôle-commande pour des applications dans le domaine de l'énergie nucléaire : depuis les années 80, les logiciels de ces systèmes sont développés avec des outils basés sur le langage Lustre. Schneider Electric est aussi impliqué dans d'autres domaines comme l'industrie, le transport, les télécommunications ou la distribution de l'énergie électrique.

EXPLOITATION DES RESULTATS

Retombées industrielles et économiques

Les retombées d'AUTOFOR s'inscrivent dans la stratégie de Schneider Electric, à savoir

  • le développement d'activités nouvelles de services et d'expertises : les travaux d'AUTOFOR, basés sur des techniques éprouvées dans des domaines critiques, sont un vecteur du développement de services dans le domaine des automatismes de sécurité.
  • l'accroissement de la compétitivité en intégrant les outils d'AUTOFOR dans les activités de Schneider Electric. Par exemple, l'atelier de programmation des automates Schneider pourra directement bénéficier de la boite a outils Lustre grace a une connexion de type "Scade vers Quantum". D'autres produits industriels (e.g. le SEPAM pour la protection des installations électriques moyenne tension) pourront aussi bénéficier de l'approche synchrone. Autre exemple, les réseaux de communication robustes et disponibles mis au point dans le cadre d'AUTOFOR sont un atout fort, compte tenu de la présence croissante des réseaux dans les architectures. Enfin, les travaux d'AUTOFOR permettent à Schneider Electric d'être en bonne position en terme de normalisation et de certification.

Retombées scientifiques

Le projet devrait conduire à des progrès scientifiques dans des domaines de recherche très actuels, comme la distribution de programmes synchrones, la vérification de propriétés numériques, ou l'automatisation du test.

ECHEANCIER DES REALISATIONS

Résultats obtenus

Signalons qu'en raison de la date tardive de démarrage du projet, ce rapport d'avancement ne concerne que 6 mois de travail effectif.

T1 - Réseaux de communication pour des applications de sûreté

T1.1 Etudier la faisabilité technique des solutions.

Cette tâche est achevée. Pour des raisons de confidentialité liés à des enjeux stratégiques, ces travaux ne peuvent être décrits ici. Une demande spécifique peut être faite pour obtenir ces renseignements.

T1.2 Démontrer la sûreté du moyen de communication

Les travaux réalisés dans cette tâche concernent l'influence des réseaux haut débit sur les systèmes de contrôle-commande. Ces travaux ont été effectués dans le cadre du projet européen ANIA (ATM Network for Industrial Automation) qui implique, outre Schneider Electric, (coordinateur), ITMI, TEKELEC et 4PLUS. Plusieurs aspect ont été étudiés : sûreté de fonctionnement, performance, ... En particulier, Schneider a réalisé une étude de sûreté en utilisant les concepts ANIA.

T1.3 Développer des solutions nouvelles, des prototypes

Cette tâche est partiellement réalisée. Elle correspond à un projet interne de Schneider qui est confidentiel à ce jour. Elle sera poursuivie dans la suite d'AUTOFOR.

T1.4 Architecture de sûreté

Cette tâche est en cours de réalisation. Elle concerne les systèmes distribués basés sur Ethernet. Un représentant Schneider participe à cette activité au travers des groupes de travail :

  • IDA (Interface for Distributed Application)
  • IAONA, organisation chargée de la promotion d'Ethernet, qui comporte 130 sociétés.

T2 La sûreté des applications

T2.1 - Cette tâche n'a pas encore commencé

T2.2 - La définition des spécifications du nouvel outil de test, combinant les prototypes LUTESS et LURETTE est en cours. Nous cherchons activement à recruter un ingénieur pour développer cet outil. Concernant les recherches sur le test, mentionnons le travail de DEA de Jerôme Vassy, effectué au LSR, sur la génération de séquences guidée par un objectif. Concernant le débogage, un premier prototype d'outil a été développé (DEA de Fabien Gaucher, Vérimag), qui offre les fonctionnalités nécessaires à l'observation macroscopique de l'exécution d'un programme LUSTRE. En vérification de programmes, une nouvelle approche a été expérimentée, qui combine les modes déclaratif et impératif de description de l'environnement d'un programme. Enfin, un travail d'optimisation du module de traitement des contraintes numériques a été initialisé, qui sera utile tant pour la vérification que pour le test.

T2.3 Transfert de l'environnement Scade vers un atelier d'automatisme

Cette tâche est partiellement réalisée et sera poursuivie dans la suite du projet. L'idée est d'utiliser l'’environnement Scade pour développer les parties les plus critiques d'une application d'automatisme. Cette partie est en général facilement identifiable (partie protection). Elle peut alors être traitée avec Lustre et bénéficier des apports de l'approche puis être intégrée directement dans l'environnement "naturel" de l'utilisateur, i.e. l'atelier de programmation de l'automate. Dans le cadre d'AUTOFOR, une passerelle a été réalisée entre Scade et l'automate Quantum de Schneider.

 

T3 Le lien avec la sûreté du process

T3.1. Vérimag a développé un outil de traduction du formalisme des matrices causes-effets en Lustre, ainsi qu'un prototype d'éditeur graphique de ces matrices. La traduction en Lustre a deux avantages :

  • Elle permet de préciser la sémantique des constructions autorisées dans les matrices causes-effets, en particulier les directives temporelles qui déterminent la durée et la position dans le temps des effets (signaux de sortie du système), par rapport aux causes (signaux d'entrée).
  • Elle permet la connexion de l'outil de manipulation de matrices causes-effets à toute la chaîne de compilation Lustre, et aux outils d'analyse développés pour Lustre :génération de tests, preuve, simulation, représentation des comportements par des chronogrammes, etc.

A terme, la traduction vers Lustre pourrait être branchée sur un éditeur de matrices causes-effets du commerce.

T3.2 Apport des méthodes formelles sur un exemple concret

L'apport des méthodes formelles est illustré sur l'exemple d'un aiguillage de voie ferrée piloté par un automate. Cet automate est programmé en Lustre. La démonstration explique comment l'alliance des méthodes formelles et des études de sûreté permet de prendre en compte de façon pertinente des aléas liés à l'environnement du système (e.g. panne des capteurs). Cette démonstration a été présentée sur le stand Schneider lors des journées "Fête de la Science" à Grenoble (20, 21, 22 octobre 2000).

T4 Satisfaire les contraintes normatives, de certifcation

T4.1 Séminaire

Un séminaire interne sur la norme CEI 61508 a eu lieu chez Schneider. Il devrait être suivi par d'autres séminaires.

T4.2 Normalisation

Schneider a mené une veille technologique concernant la normalisation Des travaux sont en cours en partenariat avec EDF et le GIMELEC (syndicat des constructeurs de l'industrie électriques), correspondant de la CEI en France.

 

T5 Valorisation des résultats

L'activité de valorisation a été consacrée à la réalisation d'un CDROM de présentation du projet. Une première version du CDROM a été présentée sur le stand Schneider lors des journées "Fête de la Science" à Grenoble (20, 21, 22 octobre 2000). Le CDROM sera disponible dans sa version définitive au mois de Décembre 00.

Perspectives

T1.3. Le travail sera poursuivi par l'industrialisation du prototype existant et l'utilisation dans un projet réel.

T1.4 L'activité sur une architecture de sûreté basée sur Ethernet sera poursuivie au travers des groupes de travail identifiés (IDA, IAONA).

T2.1 - La traduction du Grafcet en Lustre, qui a été différée dans la première phase, reste un objectif important. Nous envisageons d'adopter l'approche proposée dans la thèse de Daniel Gaffé (Université de Nice, 1995).

T2.2 - L'intégration des outils de test LUTESS et LURETTE commencera dès que nous aurons pu recruter l'ingénieur chargé du développement. Les recherches sur le test seront poursuivies, concernant les langages de description de séquences, les stratégies de sélection de ces séquence, et l'évaluation de la couverture de test. Sur le sujet du débogage, il est important de complèter les résultats obtenus par des moyens d'observer finement le comportement d'un programme au cours d'une réaction.

T2.3

Le transfert de Scade vers le Quantum doit être documenté. De plus, il doit être disséminé au sein de Schneider auprés des forces commerciales, et enfin utilisé dans le cadre d'un contexte industriel.

 

T3

Comme il a été dit plus haut, l'outil de traduction des matrices cause-effet pourra être connecté à un éditeur du commerce. Dans un avenir proche, la tâche la plus importante est de valider l'approche sur des cas réels. Schneider-Electric est en train de rechercher de telles études de cas parmi ses clients. Par ailleurs, il serait intéressant d'étudier des propriétés de consistance des descriptions en matrices cause-effet, et de vérifier automatiquement ces propriétés. De la même façon, la méthode mixte basée sur l'alliance des méthodes formelles et des méthodes probabilistes d'études de sûreté devra être validée sur une application industrielle.

T4 -

Les travaux sur la normalisation vont se poursuivre : présence dans les comité normatifs, prise de connaissance de nouvelles normes (GAMP), étude de la position de notre offre par rapport à ces normes;