Expression et Modélisation formel des risques.

 

Jean-Louis Boulanger

Université de Technologie de Compiègne
Heudiasyc UMR CNRS 6599
BP 20529
60205 Compiègne cedex
 
Tél : +33 (0)3 44 23 44 23 (poste 54 55)
Fax : +33 (0)3 44 23 44 77
 
Email : Jean-Louis.boulanger@utc.fr

                                                                                                  

 

Mots clés : Conception sûre, maîtrise des risques, méthodes formelles, vérification, validation.

 

 

Résumé étendu

 

Contexte

 

Actuellement, les méthodes formelles sont utilisées pour concevoir les parties logicielles d'un système. L'aspect "vérification interne du modèle" est basé sur l'hypothèse que le modèle contient des exigences qui doivent être respectées par le logiciel. Afin d'obtenir un ensemble intéressant d'exigence, nous préconisons de mettre en place un lien entre les analyses de risque et le(s) modèle(s) formel(s). Cela a pour conséquence de modifier certaine pratique. En effet, les analyses de risques accompagnent en général le cycle de développement du système et des applicatifs associés.

 

La conception d’un système doit passer par une analyse de faisabilité. Cette analyse doit permettre de définir les caractéristiques de l’environnement et d’identifier les risques induits. Cet article est l’occasion de montrer qu’il est possible de réaliser une analyse système des risques sous forme d’un modèle formel. Ce modèle formel pourra être utilisé comme référence, comme outils d’aide au raisonnement et comme outils d’analyse de l’impact d’une évolution. L’enjeu de ce travail est de fournir une approche permettant de formaliser les risques et de les tracer avec les exigences induites sur les composants (logiciel ou non) du système. La méthodologie proposée est basée sur l’utilisation de la méthode formelle nommée « Méthode B ».

 

Analyse de risque

 

La réalisation des arbres de défaillance (Fault Tree Analysis) est une méthodologie graphique qui permet une description systématique des impacts des défaillances qui peuvent survenir durant la vie d’un système (pour en savoir plus se reporter à [10]). Cette méthode combine les défaillances « matérielles » (hardware) et les défaillances humaines.

 

La méthode B

 

La méthode B ([1]) a été développée par Jean-Raymond Abrial, c'est une méthode formelle orientée modèle comme Z ([6]) et VDM ([4]) mais qui permet un développement incrémental de la spécification jusqu'au code, au travers de la notion de raffinement [5], et ceci dans un  formalisme unique, le langage des machines abstraites.

 

À chaque étape du développement B des obligations de preuves sont générées afin de garantir la validité du raffinement et la consistance de la machine abstraite. À partir du dernier raffinement (implémentation), le niveau de modélisation est suffisamment concret pour permettre l'utilisation d'un générateur automatique de code compilable (C, ADA et autre). Le (sous) langage B disponible au niveau implantation est appelé B0. Les restrictions syntaxiques et sémantiques portées sur le B0 permettent une construction directe du traducteur.

 

La méthode B est actuellement utilisée dans le domaine du transport ferroviaire pour développer les applications logicielles de sécurité (voir par exemple [2] et [7]). Jean-Raymond Abrial a proposé une extension nommé « B-évènementiel »  ([8] et [9]) qui doit permettre d’analyser les aspects systèmes.

 

Méthode

 

Dans le cadre de [3], nous avions présenté la problématique d’un développement basé sur la notion de propriété. Dans cette article, nous cherchons à coupler les analyses de risque avec la phase de conception système (ou sous-système). Le modèle abstrait du système doit exhiber et prendre en compte l'ensemble des propriétés dérivées à partir des risques. Ce modèle abstrait est le point de départ de la conception. La description des objets devient alors de plus en plus précise, les choix de conception sont faits et le modèle abstrait est raffiné/décomposé afin de définir une implantation. La validation des différentes étapes est faite en démontrant la prise en compte des propriétés et en vérifiant la conservation du comportement des modèles intermédiaires.

 

Résultats

 

Le mouvement des trains sur une ligne doit respecter des règles qui permettent à l'ensemble des trains de circuler en sécurité. Les risques associés au mouvement des trains sont: le risque de collision, le risque de déraillement, le risque voyageur (accès à une zone dangereuse, ...). A titre d’exemple de mise en œuvre de la méthodologie proposée, nous modéliserons un problème de collision et nous nous attarderons plus particulièrement sur la collision par écharpe. Nous verrons que le modèle système proposé permet de faire le lien entre les risques, les exigences logicielles et matérielles et les procédures d'exploitation.

 

Cet article est décomposé en trois parties. Le contexte méthodologique est mis en place dans la première partie. L'étude de cas « analyse du risque de collision entre deux trains » est présentée dans la seconde partie. L'analyse et le modèle formel sont présentés dans la dernière partie. L’article se termine par une conclusion qui fera le point sur la méthodologie et sur sa mise en application.

 

 

 

REFERENCES SUCCINTES

 

[1]       ABRIAL J.-R., "The B Book - Assigning Programs to Meanings", Cambridge University Press, august 1996.

[2]       DEHBONEI B., MEJIA F., « Formal Development of Software in Railways Safety Critical Systems », T.K.S. MURTHY B., MELLITT C., BREBBIA G., SCIUTTO S., Eds., Railway Operations, vol. 2, COMPRAIL94, Computational Mechanics Publications, 1994, p. 213-219.

[3]       “Deriving safety properties of critical software from the system risk analysis, application to ground transportation systems”, J-L Boulanger, V. Delebarre, S. Natkin, J.P. Ozello, HASE’97 : 11 et 12 août 1997 dans le Maryland aux USA.

[4]       Cliff B.Jones,"Systematic Software Development using VDM" Prentice Hall International;Second Edition, 1990.

[5]       C. Morgan, "Deriving programs from specifications", Prentice Hall International; 1990.

[6]       J. M. Spivey, " The Z notation- a reference Manual," Prentice Hall International; 1989.

[7]       P. Behm, "Application d'une méthode formelle aux logiciels sécuritaires ferroviaires", Ateliers Logiciel Temps Reel ­ 6èmes Jounées Internationales du Génie Logiciel, Part 5.1, 17-19 November 1993.

[8]       Jean-Raymond Abrial. "Event driven circuit construction." MATISSE project, August 2000.

[9]       Jean-Raymond Abrial. "Event driven distributed program construction." MATISSE project, August 2001

[10]     International standard IEC 61025, ”Fault Tree Analysis (FTA)”, International Electrotechnical Commission, Geneva, Suisse, 1990.