Certification et méthodes formelles

Conférenciers

• Gilles Motet INSA Toulouse Lesia
       Certification : origines, importance pour les systèmes informatiques,concepts de base et recherches induites.
       transparents
  - résumé: Après avoir montré les responsabilités croissantes assignées aux systèmes informatiques et les dommages causés, on introduit les interrogations des utilisateurs, des sociétés, des ingénieurs et des autorités en justifiant leurs craintes par des exemples. On déduit l'importance et la difficulté de leur fournir un haut degré d'assurance sur l'absence de dommages inacceptables (c'est-à-dire sur leur sécurité/safety) et la contribution espérée de la certification. Les termes du problème de la certification sont ensuite présentés dans le cadre de la "Gestion du risque". On conclut enfin en introduisant les axes de recherche devant être conduits, en les illustrant sur des études en cours sur les technologies Java et UML.

• Jean Gassino, Pascal Régnier Institut de Radioprotection et de Sûreté Nucléaire
       Utilisation de l'outil GATeL pour l'évaluation des tests de logiciels critiques à l'IRSN.
       transparents
  - résumé: L'IRSN (Institut de Radioprotection et Sûreté Nucléaire) émet un avis technique sur la sûreté des installations nucléaires, en vue de leur autorisation. Cette mission le conduit à évaluer leurs logiciels critiques et, entre autres, à analyser la couverture des tests fonctionnels effectués par le concepteur. L'outil GATeL du CEA a été utilisé pour identifier formellement les classes atteignables de tests couvrant une spécification fonctionnelle donnée, au sens de critères de couverture locaux et globaux spécifiquement définis. Les tests fonctionnels que le concepteur avait effectués lors du développement du système ont ensuite été comparés à ces classes, dans le but d'identifier les classes non visitées correspondant à une insuffisance de couverture. Enfin, pour chacune des classes non visitées, GATeL a calculé un scénario particulier permettant de la couvrir, afin de produire une preuve directe de son atteignabilité. Cette approche donne donc une possibilité de formaliser le test fonctionnel de systèmes critiques et permet d'en mesurer objectivement la couverture.

• Cyrille Rosay Centre d'Essais Aéronautique de Toulouse
       Formal methods in Civil Aeronautics
  - résumé: So far, CEAT has no example of certification credit taken from the use of formal methods in the development of embedded software in Aeronautic. Although formal languages are already use in this context (SCADE), the use of the proof is not generaly used to replace the classical test approach. Some issues remains unanswered, like: When do one considers that enought properties of a model have been verified? Is the chosen formal method concept valid?

• Jean Gauthier Dassault Aviation
       Apport des méthodes formelles pour la certification des commandes de vol.
       transparents

• Jean Souyris Airbus
       Analyse statique de code pour les équipements Airbus.
       transparents

• Jean-Louis Boulanger Université de Technologie de Compiègne et évaluateur CERTIFER
       Certification d'application Ferroviaire développée formellement ou non.
       transparents
  - résumé: Les industriels du domaine ferroviaire utilisent les méthodes semi formelles et les méthodes formelles depuis le début des années 80, notammenent pour le développement d'application comme le SACEM (RER A) ou/et comme le SAET-METEOR (Ligne 14). De cette expérience, ils ont tiré la norme EN 50128 qui décrit le processus de développement des applications ferroviaires. Cette norme s'applique tant pour le développement, la validation que la certification. Elle prend en compte les développements formels ou non. La présentation sera décomposée en trois parties:
  1. présentation de l'historique ferroviaire
  2. présentation de la norme EN 50128 et de sa prise en compte des méthodes formelles.
  3. présentation du contexte de la certification ferroviaire.
  4. présentation des besoins du à l'apparition de modèle réalisé avec UML.

• Pierre Morere Aonix et évaluateur CERTIFER
       Certification d'application Ferroviaire développée formellement ou non.
       transparents
  
  

  - résumé: Dans le cadre d'activité d'évaluation logicielle pour CERTIFER et la SNCF (norme EN50128), ou d'activité d'audit et de tests pour des industriels (avioniques, spatial, ferroviaire..), nous sommes amenés à évaluer des logiciels ou système qui n'utilisent pas de méthode formelle. Les spécifications apparaissent en langage naturel et les méthodes de conception utilisées peuvent être de type orienté objet (UML, HOOD, ..) ou autres voire inexistante. Dans cette présentation, quelques uns des problèmes rencontrés par un évaluateur seront présentés.
  1) la gestion de la multiplication des documents, informations redondantes et pertinences des informations.
  2) la problématique de l'évolution documentaire en cours d'évaluation
  3) l'évaluation d'instances de produit générique
  4) la pertinence des campagnes de tests unitaires
  5) l'utilisation de preuves complémentaires (PolySpace)
  6) l'utilisation de COTS
  Le but de cette présentation est de soulever la problématique de la faisabilité de méthode formelle pouvant s'appliquer à des systèmes variés et sans prérequis quant aux choix de développement fait par des industriels.