AltaRica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement - TEL - Thèses en ligne
[go: up one dir, main page]

Thèse Année : 2000
AltaRica: Contribution to the unification of formal methods and safety assessment AltaRica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement
1 LaBRI - Laboratoire Bordelais de Recherche en Informatique (Domaine Universitaire 351, cours de la Libération 33405 Talence Cedex - France)
"> LaBRI - Laboratoire Bordelais de Recherche en Informatique

Résumé

Formal methods and safety assessment are related domains interested by the behavioural analysis of critical systems. These domains consider systems with different but complementary points of view. Formal methods take a functional point of view and adopt an approach closed to the verification of programs. These methods tries to reveal scenarios yielding to a bug or to automatically generate safe programs (safe according to some specifications). In the safety assessment area the dysfunctional behaviours of systems are considered. Preponderant scenarios yielding to a specified set of unexpected states are computed and quantified to determine the probability of such behaviours.

The works presented in this report have been produced during the industrial project, called AltaRica, aiming to bring together formal methods and safety assessment communities. The project proposes to unify domains into a software, the AltaRica workbench, that will federate a set of models and tools for the analysis of systems. This workbench is based on a unique formalism for the description of systems. This report gives a full description of the formalism used by the workbench, its textual form (the AltaRica language), some properties of its semantics and some examples of modeling.

The study of fault scenarios is a major activity in safety assessment. The problem is usually treated using the Boolean model called Fault Trees. This model does not handle the ordering of failure. This thesis gives a solution to the computation of minimal scenarios (considered as words) for the subwords order.
Les méthodes formelles et la sûreté de fonctionnement sont deux domaines connexes qui s'intéressent à l'analyse des comportements des systèmes critiques. Ces domaines adoptent des points de vue différents mais complémentaires sur les systèmes. Les méthodes formelles considèrent le point de vue fonctionnel et adoptent, en général, une approche « vérification de programme ». Dans ce domaine on cherche en général à mettre en évidence un scénario menant le programme à un bogue, ou à générer de manière automatique des programmes sûrs (par rapport à leurs spécifications). La sûreté de fonctionnement considère plutôt les aspects dysfonctionnels des systèmes. Dans ce domaine on cherche à déterminer les scénarios prépondérants qui mènent le système à une défaillance ou à évaluer des mesures probabilistes sur ses comportements (fiabilité, disponibilité, ...).

Les travaux présentés dans cette thèse ont été réalisés dans le cadre d'un projet industriel, AltaRica, qui ambitionne le rapprochement des méthodes formelles et
de la sûreté de fonctionnement. Cette unification se concrétise par le développement d'un atelier d'analyse système, l'atelier AltaRica, qui fédèrera à terme un ensemble de modèles et d'outils pour l'analyse des systèmes. Cet atelier propose une représentation unique pour la description des systèmes ; celle-ci étant destinée à être compilée vers des modèles/outils existants. Ce rapport présente le formalisme supporté par cet atelier, sa forme textuelle et graphique (le langage AltaRica), certaines propriétés de sa sémantique et quelques exemples de modélisations.

L'étude des scénarios de panne est un des principaux problèmes de la sûreté de
fonctionnement. Ce problème est généralement traité en utilisant le modèle des arbres de défaillances. Ce modèle ne permettant pas de prendre en compte le séquencement des pannes, cette thèse propose une solution au problème de l'obtention des scénarios de panne minimaux pour l'ordre des sous-mots.
Fichier principal
Vignette du fichier
these-point-2000.pdf (782.92 Ko) Télécharger le fichier
Loading...

Dates et versions

tel-00353284 , version 1 (15-01-2009)
Identifiants
  • HAL Id : tel-00353284 , version 1

Citer

Gérald Point. AltaRica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement. Modélisation et simulation. Université Sciences et Technologies - Bordeaux I, 2000. Français. ⟨NNT : ⟩. ⟨tel-00353284⟩

Collections

CNRS TDS-MACS
1004 Consultations
2433 Téléchargements

Partager

More