Soutenance HDR Amel Mammar

15 novembre 2012

Amel Mammar soutiendra son Habilitation à Diriger les Recherches intitulée "Assurer la qualité du logiciel par la preuve et le test"  le jeudi 15 novembre 2012 à 10H à l'Université Paris Est, Immeuble "La Pyramide", Salle des Thèses - n° 5-21, 5ème étage, 80, avenue du Général de Gaulle, 94010 Créteil

Jury de soutenance :
   Yamine Ait-Ameur (IRIT-ENSEEIHT, Toulouse), Rapporteur
   Yves Ledru (Université Joseph Fourier, Grenoble), Rapporteur
   Michael Leuschel (Heinrich-Heine-Universität Düsseldorf, Allemagne), Rapporteur
   Marc Aiguier (Ecole Centrale, Paris), Examinateur
   Bruno Defude (Télécom SudParis, Evry), Examinateur
   Régine Laleau (Université Paris-Est Créteil), Examinateur
   Oscar Pastor Lopez (Universidad Politécnica, Valence), Examinateur

Résumé :

La dernière décennie a vu l’extension de l’utilisation des  méthodes formelles à divers domaines d’application même quand le risque humain n’est pas toujours présent. En  effet, elles sont appliquées dans le domaine bancaire par exemple pour risque financier. Les méthodes formelles permettent le développement de systèmes sûrs avec la possibilité de prouver diverses propriétés comme les propriétés de sureté et de sécurité mais également statiques et dynamiques. Nos travaux de recherche ont pour but de contribuer à l’utilisation de ce type de méthodes afin d’accroître la sureté et la sécurité des systèmes informatiques en général et en particulier les systèmes d’information et les transports ferroviaires.

Pour le développement d’application système d‘information sûres, j’ai proposé dès mes travaux de thèse un processus formel par raffinement B qui permettait de générer une implémentation B0_SQL, facilement traduisible en JAVA/SQL, à partir d’une spécification B obtenue par traduction de diagrammes UML décrivant le système. J’ai par la suite formalisé cette traduction en définissant des règles précises afin d’obtenir d’une part la structure des différentes tables relationnelles et d’autre part le code des transactions. J’ai également défini un processus systématique de calcul de préconditions pour les opérations B obtenues afin qu’elles prennent en compte des contraintes non graphiques exprimées directement en B. Enfin, je me suis intéressée à des propriétés dynamiques pour lesquelles j’ai défini  des obligations de preuve supplémentaires à établir pour pouvoir les vérifier sur le système.

Mes travaux de recherche s’attaquent également à la détection de vulnérabilités (erreurs de programmation) dans les programmes C. Pour cela, j’ai défini deux approches automatiques, une utilisant le test passif et une seconde basée sur la preuve et la méthode B.

Enfin, dans le cadre d’une expérience industrielle au sein de la RATP puis Thales Transport, j’ai contribué à la formalisation et la preuve d’un ensemble de propriétés de sécurité pour le Métro parisien.

Événements