Rechercher

[Eti08a] Certifying Airport Security Regulations using the Focal Environment

Mémoire de Thèse : Soutenue le: 07 July 2008, pp. 200, pp.: Directeur: V. Viguié Donzeau Gouge - D. Delahaye
Rapporteur 1:
Rapporteur 2:
Membre du jury:
Membre du jury:
Membre du jury:, : Certifying Airport Security Regulations using the Focal Environment,

Auteurs: J. Etienne

motcle:
Résumé: Le programme de sûreté (dans le transport aérien le terme sûreté correspond à des problèmes sécuritaires), établi au niveau de chaque aéroport, est régi par une série de réglementations internationales et de recommandations dont le but est de se protéger contre des actes d'intervention illicite dans l'aviation civile. Un aspect essentiel de l'application de ces normes est d'évaluer la conformité des procédures et artéfacts réglementés. Cependant, pour que le processus d'évaluation soit le plus efficace possible, il est aussi nécessaire de s'assurer de la qualité des documents normatifs. Cette thèse, qui a été réalisée dans le cadre du projet EDEMOI, décrit la méthodologie adoptée pour la formalisation et l'analyse des réglementations Annexe~17 (ICAO, niveau international) et Doc~2320 (ECAC, niveau européen) dans l'atelier Focal. Focal est utilisé principalement pour la production de composants certifiés formellement. La formalisation met en évidence la nécessité d'organiser la réglementation sous forme d'une hiérarchie de propriétés de sûreté. La validation de la réglementation s'effectue en raisonnant sur la hiérarchie établie afin de détecter des incohérences (ou de garantir leur absence), d'identifier des hypothèses cachées ou de détecter des failles potentielles de sûreté. L'évaluation de l'adéquation de Focal pour la modélisation des réglementations est une autre contribution de la thèse. Certaines améliorations sont aussi suggérées. De plus, comme la sécurité dans les aéroports est un problème de grande envergure, cela a aussi servi à valider le pouvoir d'expressivité et de raisonnement de Focal. Enfin, la thèse propose aussi une transformation automatique des spécifications Focal en diagrammes UML. L'objectif est ici de fournir une documentation graphique des modèles formels aux développeurs. À long terme, il est envisagé de produire des diagrammes à des niveaux d'abstraction plus élevés qui seront pertinents pour les autorités de certification. Un cadre formel est aussi décrit pour démontrer la correction de la transformation.

Equipe: sys

BibTeX

@phdthesis {
Eti08a,
title="{Certifying Airport Security Regulations using the Focal Environment}",
author="J. Etienne",
year=2008,
pages="200",
address="{CEDRIC Laboratory, Paris, France}",
note="{
Directeur: V. Viguié Donzeau Gouge - D. Delahaye
Rapporteur 1:
Rapporteur 2:
Membre du jury:
Membre du jury:
Membre du jury:}",
}