Pascal LAMY, Jean-Christophe BLAISE
Institut National de Recherche et de Sécurité
Avenue de Bourgogne
F-54501 VANDOEUVRE
pascal.lamy@inrs.fr, jean-christophe.blaise@inrs.fr
Contexte
La complexité des applications industrielles incluant des APIdS est telle qu’il est nécessaire de mettre en pratique de nouvelles méthodes lorsqu’il s’agit de concevoir des fonctions de haut niveau de sécurité. Des normes spécifiques à ces technologies telles que les normes FDIS CEI 62061 [1] et CEI 61508 [2] recommandent, par exemple, l’utilisation de méthodes formelles pour vérifier qu’un logiciel répond bien à son cahier des charges et contribuer ainsi à l’obtention d’un haut niveau de sécurité.
En phase de conception des logiciels, les méthodes formelles [3] [4] [5] permettent, grâce à un langage particulier, d’exprimer très rigoureusement les propriétés issues du cahier des charges. Elles offrent ensuite la possibilité de prouver de manière automatisée que ces propriétés sont non ambiguës, cohérentes et non contradictoires. Elles garantissent par preuves mathématiques que ces propriétés sont respectées au fur et à mesure (tout au long) des étapes de conception. Les logiciels ainsi développés sont garantis sans défaut par rapport à ces propriétés. On cherche ainsi à limiter au plut tôt et en phase de conception les évènements dangereux qui pourraient apparaître en cas de comportement inapproprié du logiciel lors de l’exploitation de la machine.
A l’heure actuelle, de telles techniques ont été utilisées dans le domaine ferroviaire pour la partie sécuritaire de la ligne de métro Météor [6], dans le domaine énergétique [7], dans l’aéronautique [8], dans l’automobile pour la réalisation d’un régulateur de vitesse [9], pour des contrôles d’accès [10], mais pas encore dans le domaine manufacturier.
L’INRS a souhaité évaluer l’applicabilité et les contraintes d’utilisation de ces méthodes dans le cadre d’une application « machines » utilisant un logiciel développé avec un langage spécifique pour les automates programmables industriels.
Présentation succincte des méthodes formelles employées
La démarche a consisté à utiliser deux méthodes de développement formel différentes :
Utilisation de la méthode B
La méthode B [11], inventée en 1980 par J.-R. ABRIAL, utilise le langage B fondé sur les concepts mathématiques de la théorie des ensembles ; ce langage intègre des mécanismes de preuve et peut couvrir sans rupture tout un cycle de développement, jusqu’au code pour les éléments logiciels. Cette méthode est par ailleurs supportée par un outil logiciel.
Un développement selon cette méthode débute par la construction d’un modèle B reprenant toutes les descriptions du besoin. D’autres modèles sont ensuite élaborés par étapes successives, toujours à l’aide du langage B, jusqu’à l’obtention du programme exécutable. La cohérence des modèles obtenus à chaque étape et la conformité du programme au modèle initial sont garanties par des preuves mathématiques. Ce développement est illustré dans le schéma suivant (cf. figure 1):
Figure 1 : représentation du cycle de développement mis en œuvre en utilisant la méthode B
Utilisation d’une méthode de vérification formelle a posteriori
La vérification formelle a posteriori consiste à décrire des propriétés (propriétés de sûreté en l’occurrence) qui devront être prouvées mathématiquement. Elle est basée sur le principe de « Model Checking » [12] qui est un processus automatique consistant à vérifier l’équivalence entre un modèle formel des propriétés que doit vérifier le système et un modèle formel du système. Quelques travaux [13, 14] ont été effectués à l’aide de ce principe, appliqués aux langages de la norme CEI 61131-3 [15] ainsi qu’aux langages de spécifications tel que le Grafcet [16].
Nous avons utilisé un logiciel de conception d’automatisme dans lequel un prototype de vérification formelle a posteriori a été intégré. L’avantage de ce prototype est de masquer, pour l’utilisateur, le formalisme mathématique de la vérification formelle. Ce type d’outil suppose dans un premier temps de concevoir le système puis d’insérer, à la fin de la conception, les propriétés que l’on souhaite voir respectées. Ce développement est illustré par le schéma représenté figure 2 :
Figure 2 : représentation du cycle de développement mis en œuvre en utilisant une méthode de vérification formelle a posteriori
Application sur un cas réel
Le logiciel applicatif d’une presse mécanique (Fig. 3) à embrayage-frein équipée d’un APIdS du marché a été développé à l’aide de ces deux méthodes.
Fig. 3 : presse mécanique à emboutir à embrayage-frein
Réalisation du logiciel applicatif à l’aide de la méthode B
Réalisation d’un nouveau cahier des charges (cf. figure 1, cadre n°1 « Phase préliminaire à la méthode »)
Cette partie a consisté à rédiger en langage naturel un nouveau cahier des charges de la presse qui rassemble toute l’information nécessaire pour le développement logiciel. Ce document doit décrire le système et il doit présenter de manière claire, non ambiguë et le plus complètement possible les exigences sur le logiciel sécuritaire contrôlant la presse.
Le nouveau cahier des charges contient à la fois une partie descriptive du fonctionnement de la presse et une partie définissant précisément les exigences fonctionnelles et sécuritaires du logiciel. Ces descriptions servent de référence au développement du logiciel contrôlant la presse, à la fois lors des phases de spécification et conception logicielle et lors des phases de test d’intégration et de validation.
La rédaction par l’expert (ou la personne ayant en charge la modélisation) B de ce nouveau cahier des charges lui permet de s’approprier le fonctionnement de la presse et de reformuler les exigences initiales. L’utilisation du langage naturel assure :
que ce nouveau cahier des charges peut être relu par les experts de l’INRS,
un consensus entre les experts INRS et le modélisateur B sur le nouveau cahier des charges.
Modèle B : spécification et conception (cf. figure 1, cadre n°2 « Réalisation du modèle B »)
Ce travail de spécification et de conception à l’aide de la méthode formelle B consiste à décrire les aspects fonctionnels du système à l’aide d’une succession de points de vue allant du plus général au plus détaillé : c’est le raffinement. Un modèle B constitué de plusieurs niveaux de raffinement entièrement prouvés a ainsi été réalisé. Ce modèle décrit l’ensemble de la presse et de son environnement en formalisant les exigences du cahier des charges rédigé à l’étape précédente.
Les premiers raffinements décrivent le système en détaillant les parties observables de l’extérieur : la presse, les mains de l’opérateur, la direction du mouvement du coulisseau, les protecteurs, l’arrêt au point mort haut.
Dans l’exemple ci-dessous, représentatif d’un premier niveau de raffinement, un observateur extérieur à la situation voit que la presse passe d’un état de fonctionnement à un état d’arrêt. On décrit ainsi de façon très générale l’événement consistant en l’arrêt de la presse.
arreter_presse =
SELECT PRESSE=en_marche
THEN PRESSE:=arrete END;
Les derniers niveaux de raffinement décrivent le fonctionnement du système de manière très détaillée. Ils formalisent notamment le détail de chaque traitement unitaire du logiciel et de chaque action physique observable.
Après raffinement, le traitement présenté ci-dessus devient :
arreter_presse =
SELECT
(mode:{M2,M3,M4} => MOTEUR=en_marche) &
EMBRAYAGE=en_marche &
sortie_embrayage=arrete &
(CAME_PMH=OK or CAME_PMB=KO => ARRET=OK)
THEN
EMBRAYAGE:=arrete ||
capteur_embrayage:=arrete ||
capteur_embrayage_bis:=arrete
END;
Le mécanisme de preuve effectué lors des raffinements successifs assure la cohérence d’une nouvelle itération vis-à-vis des modèles précédents, mais aussi au sein du raffinement en cours de création. L’intérêt de la méthode B est d’obtenir un modèle final prouvé et cohérent par rapport au modèle initial et à ses itérations.
Codage et validation (cf. figure 1, cadre n°3 « Codage et validation »)
Traduction vers le langage de programmation de l’APIdS cible
Afin de pouvoir importer le modèle B sur l’automate, il a fallu définir les principes de traduction du dernier raffinement B en langage de programmation de cet automate cible. Cette étude de traduction établit la faisabilité d’un outil de traduction automatique de B en langage automate. Dans notre cas, la traduction a été faite manuellement à l’aide de ces principes.
Validation sur l’automate
Cette tâche a consisté à charger le logiciel généré à l’étape précédente dans l’automate dédié à la sécurité de la presse et à passer des scénarios de test sur un banc de simulation permettant d’émuler les capteurs et actionneurs de la presse. Il est aussi possible de réaliser des défaillances de composant ou des incohérences de comportement.
L’avantage d’une telle validation est de réaliser une réelle validation du logiciel dans son environnement matériel (automate).
Cette validation reste nécessaire, malgré l’usage de la méthode B, afin de valider l’interface du logiciel avec le matériel, les conditions d’initialisation et les aspects temps réel. Plusieurs problèmes ont effectivement été détectés en phase de validation. Il s’agit de problèmes d’interface, d’un problème de cohérence d’initialisation du modèle B, de problèmes de validation des principes de traduction et de problèmes de traduction manuelle.
Réalisation du logiciel applicatif à l’aide de la vérification formelle a posteriori
Modélisation du logiciel applicatif et conception détaillée (cf. figure 2, cadre n°1 « Modélisation »)
Le logiciel applicatif de la presse a été modélisé sous forme d’un ensemble hiérarchique et structuré de fonctions. Ces fonctions (également appelées composants génériques) peuvent être élémentaires ou composées. Une fonction élémentaire est décrite par un langage de la norme CEI 61131-3. Une fonction composée est décrite dans un éditeur d’assemblage de fonctions. Chaque fonction peut être utilisée plusieurs fois dans l’application. Les fonctions sont représentées dans l’outil sous forme de boîtes noires.
Validation du modèle (cf. figure 2 cadre n°2)
L’outil utilisé pour la modélisation met en oeuvre un certain nombre de ressources pour aider l’utilisateur dans le développement de son application. Ainsi, il est possible par des mécanismes de simulation et de visualisation dans des Interfaces Homme Machine représentatifs de l’environnement de la presse de valider :
les composants élémentaires, donc de réaliser des tests unitaires,
l’intégration des différents composants logiciels dans les assemblages (équivalent des tests d’intégration).
Cette interface permet d’une part, d’agir sur des boutons représentant les différentes possibilités d’actions envisageables pour l’opérateur et d’autre part, de visualiser l’état dynamique des différentes variables et de simuler des défauts.
Réalisation des preuves
Une propriété à vérifier est modélisée par une variable correspondant à l’événement redouté. Cette variable porte sur les entrées ou les sorties et peut être simple, comme par exemple s’assurer que deux sorties du modèle ne seront pas vraies en même temps ou plus complexe en s’assurant qu’une combinaison logique de variables ne pourra jamais arriver.
Le moteur de preuves va automatiquement vérifier que la propriété est respectée et en cas de non vérification de la preuve, un exemple amenant à cette non vérification de la preuve est proposé et peut être simulé. Toutefois, cet exemple n’est pas exhaustif car l’outil fournit le premier exemple qu’il trouve et nécessite une interprétation afin de trouver la cause du problème qui peut-être :
soit une erreur dans la modélisation,
soit un cas dont les conditions d’obtention ne sont pas réalistes.
L’outil utilisé pour réaliser les preuves est un prototype non commercialisé qui n’est pas encore suffisamment mature. Lors du passage des preuves, nous avons rencontré les problèmes suivants :
Des contraintes fortes liées à l’utilisation du moteur de preuve qui peuvent perturber l’utilisateur dans sa modélisation et lui imposer des choix de
odélisation qui ne sont pas forcément judicieux.
La difficulté à faire une preuve sur plus de deux variables ; la difficulté à faire des preuves sur des combinaisons temporelles entre variables
La saturation de l’outil lors de la réalisation de certaines preuves, phénomène connu sous le nom d’explosion combinatoire et lié à la technique utilisée qui consiste à parcourir l’ensemble des états atteignables
La partie non formelle de l’outil nous aura permis de poursuivre le travail afin de générer le logiciel et de procéder à son intégration dans l’automate cible (cf. figure 2, cadre n°3 « Intégration ») mais les problèmes rencontrés ne nous ont pas permis d’obtenir un modèle prouvé du programme de la presse.
Discussion
L’utilisation de la méthode B a amené plusieurs constatations :
– la place de l’expert en B est très importante pour la réalisation du modèle puisque de nombreux choix de modélisation ont été réalisés. Par contre, l’utilisation de la méthode B et de la preuve ont permis de s’assurer que ces options de modélisation sont bien cohérentes avec les règles de sécurité modélisées dans le modèle B,
– la présence d’un expert en B est nécessaire pour comprendre et mener à bien la démarche suivie d’où un coût d’appropriation (formation), d’utilisation de cette méthode,
– la traduction manuelle du dernier raffinement vers le langage de programmation de l’automate a entraîné des erreurs dans le code généré. Il est bien évident que dans le cadre d’un processus industriel, un traducteur automatique validé devrait être réalisé d’où un coût et des délais supplémentaires,
– le principal problème détecté lors de la validation est venu d’une mauvaise définition, en phase de conception, de l’interface entre les variables logicielles et l’implémentation matérielle (définition des Entrées/Sorties),
– une autre erreur de modélisation a été découverte pendant la validation ; cette erreur était due à un compromis entre l’investissement en temps, coût d’utilisation de la méthode et la volonté d’obtenir un modèle complet du système. La validation aura ainsi permis de valider certaines hypothèses de modélisation.
Une réflexion sur le développement de logiciel pour presse de façon classique et par l’utilisation de la méthode B peut être menée. Deux éléments peuvent la guider :
Ce type de logiciel est réalisé par de petites entreprises. De plus, l’utilisation des Automates Programmables Industriels dédiés à la Sécurité orientent le concepteur vers l’utilisation de l’atelier logiciel spécifique à cet automate. Cet atelier logiciel peut contenir des blocs fonctionnels validés et certifiés (la gestion de la commande bimanuelle est par exemple assurée par un seul bloc). A l’heure actuelle, ces entreprises disposent de peu de temps pour développer et valider le logiciel. Il se pose alors le problème du niveau de sûreté du logiciel atteint. Apprécier ce niveau de sûreté reste difficile et constitue une des préoccupations de l’INRS dans son travail de validation de systèmes de commande [17].
L’utilisation de la méthode B a nécessité environ 4 semaines pour le développement logiciel complet par des personnes non expertes de la presse (sans utiliser les blocs fonctionnels certifiés) et une semaine supplémentaire pour exécuter des tests fonctionnels. La preuve couvre de manière exhaustive les tests unitaires et les tests d’intégration et permet d’obtenir un niveau de sûreté élevé.
L’utilisation d’une méthode de vérification formelle a posteriori mène à un résultat plus mitigé. L’objectif était de pouvoir combiner les pratiques de l’automaticien avec l’utilisation d’un moteur de preuves, ceci de manière transparente pour l’utilisateur. Cet objectif n’a pas été atteint. En effet, les différents problèmes rencontrés avec le prototype de vérification formelle n’auront pas permis de construire des preuves pertinentes. L’utilisation de la vérification formelle a posteriori semble, à ce jour, difficilement applicable du fait du manque d’outil approprié..
Conclusion
Cette étude de faisabilité réalisée par l’INRS a permis d’appliquer deux types de développement formel du logiciel au cas d’un système manufacturier à base d’Automate Programmable Industriel dédié à la Sécurité.
Elle a montré que l’utilisation de la méthode B est très intéressante dans le cas d’applications sécuritaires puisque les modèles B ont été très peu modifiés pendant la phase d’intégration. Cette méthode a permis de s’affranchir de la validation des différents modules logiciels (tests unitaires). La phase d’intégration du logiciel et du matériel reste quant à elle une étape nécessaire dans tout développement logiciel, même utilisant des méthodes formelles, afin de s’assurer de l’adéquation avec le matériel.
Un des points qui pourrait être pénalisant dans le secteur manufacturier est la nécessité de faire appel à du personnel formé et compétent, voire expert en B, au départ mais aussi pour toute évolution ou modification du logiciel. Une telle contrainte destine l’utilisation de cette méthode à des entreprises disposant de projets d’envergure de conception de machines neuves dont l’investissement initial pourra être rentabilisé sur plusieurs projets. Il faut donc une politique volontaire de l’entreprise pour favoriser l’utilisation de cette méthode de conception puisqu’elle entraîne un changement de mentalité vis-à-vis du développement logiciel.
Concernant l’utilisation des méthodes de vérification formelle a posteriori, bien que cette solution soit plus abordable pour l’automaticien, l’outil utilisé dans notre cas n’est pas finalisé et cette technique n’est donc pas encore exploitable. L’utilisation de cette technique de vérification a posteriori nécessite, tout comme la méthode B, une nouvelle approche de la part du concepteur afin de déterminer les propriétés de sécurité qu’il voudra vérifier. De plus, il ne sera pas dispensé de réaliser des tests et de la simulation.
Bibliographie
[1] FDIS CEI 62061. Sécurité des machines – Sécurité fonctionnelle des systèmes de contrôle électriques/électroniques/électroniques programmables. Version FDIS, mai 2004, 94 p.
[2] CEI 61508. Sûreté fonctionnelle : systèmes relatifs à la sûreté. Partie 1 à 7. 1998.
[3] BELLOT P., COTTIN J.P., MONIN J.F. – Développement et validation de logiciels. Méthodes formelles. Techniques de l’Ingénieur, H 2550, 1995, 13 p.
[4] JONES C.B. – Systematic Software Development using VDM, second edition. Prentice Hall International, Englewood Cliffs, 1990, 300 p.
[5] SPIVEY M. – Introducing Z : a specification language and its formal semantics. Cambridge University Press, Cambridge UK. 1998.
[6] ABRIAL J.R. – Méthodes formelles avec preuves ; Etude de cas et réflexions. Journée de débats du club automation, 9 avril 2002, 26 p.
[7] DALZON J.P. – Maîtrise de la qualité du contrôle commande de centrales électriques. Journée Club Automation du 9 avril 2002, 12 p.
[8] AIR & COSMOS – Le logiciel embarqué français part à la conquête du monde, N° 1826, p 12.
[9] Projet ISdF N°8/95 – Langages formels et sûreté de fonctionnement des systèmes critiques, lot 1 à 5, Institut de Sûreté de Fonctionnement.
[10] DROSCHL G., KUHN W., SONNECK G., THUSWALD M. – Assessing the practical benefits of formal methods for software development. Safety Science, 2001, 12 p.
[11] ABRIAL J-R, “The B Book– Assigning programs to meanings”, Cambridge University Press, ISBN 0-521-49619-5, 1996.
[12] Coordination Schnoebelen P., Vérification de logiciels : Techniques et outil du model-checking, Edition Vuibert, Paris, 1999
[13] B. ZOUBEK, J.-M. ROUSSEL, M. KWIATKOWSKA, Towards automatic verification of ladder logic programs, Proceedings of IMACS-IEEE « CESA’03 » : « Computational Engineering in Systems Applications », CD ROM paper S2-I-04-0169, July 2003, 6 pages, Lille (France)
[14] J.-M. ROUSSEL, B. DENIS, Safety Properties Verification of Ladder Diagram Programs, JESA, Vol 36/7, 2002
[15] CEI 61131 Partie 3 Automates programmables – Langages de programmation, mars 1993, 411 p.
[16] NF EN 60848 Langage de spécification GRAFCET pour diagrammes fonctionnels en séquence, août 2002, 54 p.
[17] J.C. BLAISE – J.P. BELLO – J. BAUDOIN PLC-based control systems for safety applications: a third party validation method, SIAS 2005
