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 ?
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.
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.