|
Plate-forme Systèmes et Logiciels Critiques
|
Plan |
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.
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 :
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 :
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:
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 :
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
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.
EXPLOITATION DES RESULTATS Retombées industrielles et économiques Les retombées d'AUTOFOR s'inscrivent dans la stratégie de Schneider Electric, à savoir
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 :
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 :
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;
|