Description
Date depot: 1 janvier 1900
Titre: Développement de logiciel critique en Focalize - Méthodologie et outils pour l'évaluation de conformité
Directrice de thèse:
Thérèse HARDIN (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Alors que les logiciels devraient permettre d'améliorer la qualité et les
performances de service rendus aux utilisateurs, les entreprises
continuent de produire des logiciels dont la qualité est notoirement
insuffisante, les délais de production toujours plus longs et mal
maîtrisés. Tout semble montrer que la complexité des logiciels croit
plus vite que la capacité à démontrer leur bonne adéquation aux
besoins requius et leur bon fonctionnement.
Cette thèse repose sur l'expérience de l'auteur, en tant qu' évaluateur de systèmes critiques pilotés par du logiciel et tende de répondre au besoin de support
théorique et de formalisation des études de risque, afin de conforter
les décisions de mise en exploitation.
Le problème est posé dans le cadre de l'utilisation de l'atelier de développement Focalize. Il permet l'écriture de spécifications sous forme de formules du premier ordre puis le développement progressif du code, en utilisant héritage, paramétrisation et modularité. La thèse s'intéresse à deux aspects de la certification d'un logiciel critique développé à l'aide de Focalize.
Tout d'abord, La conformité de l'outil aux exigences requises par les principales
normes applicables dans le domaine de la Sûreté de Fonctionnement est étudiée. Pour cela, un cycle de développement système couvrant l'ensemble des phases de développement de la spécification à la maintenance est proposé. Ce travail permet de montrer que l'outil Focalize possède toutes les caractéristiques nécessaires à une
certification.
La thèse porte ensuite sur la réalisation d'analyses de risques sur un logiciel issu d'un développement en Focalize. Une présentation des différentes méthodes
appliquées pour l'évaluation d'un logiciel est effectuée. Puis, un outil de calcul de dépendances entre Entrées/Sorties vraies d'un composant est spécifié formellement en Coq et sa preuve de correction est fournie. Une implémentation prototype a été réalisée.
Doctorant.e: Ayrault Philippe