Skip to content
Atelier : Certification & Argumentation
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
README.md

README.md

Atelier : Certification & Argumentation

De manière générale, les activités de certification consistent, pour un appliquant (celui qui demande une certification), à collecter une documentation exhaustive, rassemblant et expliquant non seulement les résultats, mais aussi les données d’entrée, les hypothèses faites, les techniques appliquées, les preuves formelles réalisées, les tests, etc. Même si des avancées indéniables ont été réalisées dans le domaine des méthodes formelles afin d’établir automatiquement des preuves de correction, la certification reste une activité essentiellement documentaire et centrée process.

De nombreux travaux cherchent à organiser cette documentation, cet ensemble d’éléments de preuves, dans un cadre cohérent sous la forme d’une argumentation. Nous pouvons citer Safety Argument Manager, Goal Structuring Notation (GSN), ASCAD notation et Justification Diagram pour les travaux académiques et le Structured Assurance Case Meta-model (SACM) ou l’ISO 15026 pour les organismes de standardisation.

L’ensemble de ces travaux ont un point commun, ils trouvent leur origine dans le modèle d’argumentation présenté par Stephen Toulmin en 1958 dans son ouvrage The Uses of Argument. En effet, les travaux menés pour comprendre et modéliser l’Argumentation peuvent être d’une grande aide pour nous aider à structurer les différents éléments, qu’ils soient formels ou informels, constituant un dossier de certification.

Au travers de présentations et d’une grande place laissée au dialogue, le présent atelier vise à adresser les questions suivantes :

  • La preuve formelle suffit-elle ? Doit-elle suffire? Faut-il lui adjoindre des justifications informelles ?
  • Peut-on exprimer les standards de certification sous formes d’argumentation ? Pour quels gains?
  • L’argumentation pour la certification peut-elle être faite ex nihilo ou doit-elle être une part d'un processus continu de développement?
  • La certification de demain pourra-t-elle être complètement argumentative ?

Planning

Introduction à l’atelier

Thomas Polacsek et Mireille Blay-Fornarino (ONERA / Université Nice Côte d'AZUR)

Une approche basée patron pour la certification multi-coeur

Kevin Delmas (ONERA)

Overarching-Properties, Argumentation and Streamlining Development Assurance

Hervé Delseny (Airbus)

An Overarching-Properties Assurance Case for Qualification of a Code Generator

Cyrille Comar (Adacore)

In this talk, AdaCore will present an assurance case based on the Overarching Properties for a hypothetical, qualified code generator called Chyp. An assurance case is an argument with its supporting artifacts. In the context of an FAA effort for streamlining avionics certification, three Overarching Properties have been defined as sufficient for demonstrating the fitness for use of an item being certified, once the necessary safety considerations have been taken into account. This assurance case will show, using a notation inspired by Toulmin, how the Chyp Code generator is fit for use in Model-Based development of critical avionics components where most of the verifications are done through model simulation.

Agilité et sûreté logicielle : quand le DevOps les réconcilie

Clément Duffau (Stack Labs)

Dans cette présentation, nous montrerons comment l'industrie tente de faire évoluer les méthodologies de développement logiciel dans les domaines critiques pour embrasser l'Agilité tout en garantissant la sûreté/sécurité. Notamment, nous présenterons une approche DevOps, utilisant des diagrammes de justifications, au travers de son application dans le contexte de développement de "devices" pour le médical.

You can’t perform that action at this time.