Développement formel
Sécurisation des systèmes mécatroniques. Partie 2 - Techniques de mises en sécurité d'une application logicielle
BM8071 v1 Article de référence

Développement formel
Sécurisation des systèmes mécatroniques. Partie 2 - Techniques de mises en sécurité d'une application logicielle

Auteur(s) : Jean-Louis BOULANGER

Date de publication : 10 janv. 2011 | Read in English

Logo Techniques de l'Ingenieur Cet article est réservé aux abonnés
Pour explorer cet article plus en profondeur Consulter l'extrait gratuit

Déjà abonné ?

Sommaire

Présentation

RÉSUMÉ

Les systèmes mécatroniques sont de plus en plus complexes. Ils induisent par voie de conséquence de multiples défaillances. La sécurisation de ces systèmes vise à combattre ces erreurs et à tenter d'en limiter le risque. Cet article s'intéresse à l'aspect application logicielle, dont la sécurité passe par la maîtrise de la qualité. Sont présentées quelques techniques de programmation tolérante (redondance, détection d'ereurs ou programmation défensive). Les fautes sont souvent dues au caractère artisanal de la réalisation d'une application logicielle, et l'utilisation d'outils d'un environnement de développement ne retire pas au logiciel sa complexité intrinsèque.

Lire cet article issu d'une ressource documentaire complète, actualisée et validée par des comités scientifiques.

Lire l’article

Auteur(s)

INTRODUCTION

Dans cette seconde partie [BM 8071] sur la sécurisation des systèmes mécatroniques, nous nous intéressons à l'aspect « application logicielle » (composante informatique). Le risque lié à l'architecture matérielle (composante électronique) ayant été traité dans la première partie [BM 8 070]. Pour ce qui concerne les concepts de base et les normes applicables à la sécurisation des systèmes mécatroniques, le lecteur se reportera également en [BM 8 070].

La sécurité d'une application logicielle passe principalement par la maîtrise de la qualité (évitement et élimination des fautes). Nous présentons :

  • les principes de la maîtrise de la qualité (ISO 9001:2000) ;

  • quelques techniques de programmation tolérante (la redondance, la détection d'erreur ou la programmation défensive) ;

  • l'apport des méthodes formelles.

La réalisation d'une application logicielle est actuellement une activité à la portée de tous. La mise à disposition d'environnements de développement (Case Tools , cf. [Doc. BM 8 070]), proposant la modélisation, des vérifications et la génération automatique de code, a grandement simplifié le développement d'une application logicielle. Mais la principale particularité du logiciel est la présence de fautes (bug ). Ces fautes peuvent être systématiquement exécutées et leur présence est due au caractère artisanal de la réalisation d'une application logicielle. L'utilisation d'environnements de développement donne l'impression d'industrialiser la réalisation d'une application logicielle mais il n'en est rien. En effet, les outils d'un environnement de développement sont développés classiquement et leur utilisation a tendance à faire oublier la complexité intrinsèque du logiciel au travers de représentations graphiques plus ou moins claires. La présence de fautes est un fait et il faut soit les accepter, soit les gérer, soit les corriger.

Logo Techniques de l'Ingenieur

Cet article est réservé aux abonnés.
Il vous reste 92 % à découvrir.

Pour explorer cet article Consulter l'extrait gratuit

Déjà abonné ?


4. Développement formel

4.1 Méthodes formelles

Les méthodes formelles sont en plein essor notamment dans les applications critiques telles que les centrales nucléaires, l'avionique ou le transport ferroviaire. Le problème des applications critiques est de garantir un maximum de sécurité dans le fonctionnement de l'application. L'apport des méthodes formelles est d'offrir un cadre mathématique au processus de développement, ce qui permet de disposer d'une méthode permettant la production de logiciels corrects par construction grâce à un processus de développement vérifiable par des techniques de validation tel que la preuve ou l'exploration de modèle. Pour cela, il faut évidemment décrire de façon précise les propriétés que le système informatique doit posséder. Les méthodes formelles sont de différentes classes :

  • les spécifications algébriques (PLUSS ou PVS) ;

  • les spécifications équationnelles (LUSTRE) ;

  • les spécifications orientées modèle (B , VDM  ou Z ).

À l'inverse d'une validation orientée exploration de modèle (model checking ) comme LUSTRE, la méthode B est basée sur la preuve d'obligation de preuve qui garantit la faisabilité et la cohérence du modèle (validité du raffinement).

Dans le milieu ferroviaire français, l'utilisation des méthodes formelles, et notamment l'utilisation de la méthode B, est de plus en plus courante dans le cadre de développement...

Logo Techniques de l'Ingenieur

Cet article est réservé aux abonnés.
Il vous reste 93 % à découvrir.

Pour explorer cet article Consulter l'extrait gratuit

Déjà abonné ?


Lecture en cours
Développement formel

Article inclus dans l'offre

"Métier : responsable bureau d'étude/conception"

(370 articles)

Une base complète d’articles

Actualisée et enrichie d’articles validés par nos comités scientifiques.

Des contenus enrichis

Quiz, médias, tableaux, formules, vidéos, etc.

Des modules pratiques

Opérationnels et didactiques, pour garantir l'acquisition des compétences transverses.

Des avantages inclus

Un ensemble de services exclusifs en complément des ressources.

Voir l'offre

Sommaire
Sommaire

BIBLIOGRAPHIE

  • (1) - ABRIAL (Jr.) -   The B book – Assigning programs to meanings.  -  Cambridge University Press, Cambridge, août 1996.

  • (2) - BALEANI (M.), FERRARI (A.), MANGERUCA (L.), PERI (M.), PEZZINI (S.) -   Fault-tolerant platforms for automotive safety critical applications.  -  Proceedings of the 2003 international conference on Compilers, architecture and synthesis for embedded systems, p. 170-177 (2003).

  • (3) - BIED-CHARRETON (D.) -   Concepts de mise en sécurité des architectures informatiques.  -  Recherche Transports Sécurité, no 64, p. 21-36, juil.-sept. 1999.

  • (4) - DUFOUR (J.L.) -   Automotive safety concepts : 10-9/h for less than 100E a piece.  -  Automation, Assistence and Embedded Real Time Platforms for Transportation, AAET, Braunschweig, Allemagne, 16-17 fév. 2005.

  • (5) - GEORGES (J.P.) -   Principes et fonctionnement du Système d'Aide à la Conduite, à l'Exploitation et à la Maintenance (SACEM). Application à la ligne A du RER.  -  Revue Générale des Chemins de Fer, no 6, juin 1990.

  • ...
Logo Techniques de l'Ingenieur

Cet article est réservé aux abonnés.
Il vous reste 93 % à découvrir.

Pour explorer cet article Consulter l'extrait gratuit

Déjà abonné ?


Article inclus dans l'offre

"Métier : responsable bureau d'étude/conception"

(370 articles)

Une base complète d’articles

Actualisée et enrichie d’articles validés par nos comités scientifiques.

Des contenus enrichis

Quiz, médias, tableaux, formules, vidéos, etc.

Des modules pratiques

Opérationnels et didactiques, pour garantir l'acquisition des compétences transverses.

Des avantages inclus

Un ensemble de services exclusifs en complément des ressources.

Voir l'offre

Ressources documentaires

Simulation et CAO en automatique et mécatronique

La simulation est aujourd'hui intégrée au processus de conception des systèmes intégrant une ...

Approche virtuelle pour la conception et le développement de systèmes mécatroniques – Méthodologie

Le présent article a pour but de proposer un processus intégré de conception et de développement de ...

Approche virtuelle pour la conception et le développement des systèmes mécatroniques – Mise en oeuvre

Le présent article a pour but d’appliquer à un cas industriel la méthodologie de conception et de ...

Chaînes de transmission de puissance mécatroniques - Mise en place des modèles d'estimation pour la conception préliminaire

Les systèmes actuels de transmission de puissance réclament des solutions de moins en moins coûteuses, ...