Amélioration des processus de vérification de programmes par combinaison des méthodes formelles avec l'ingénierie dirigée par les modèles

During software development, and more specifically embedded avionics applications development, verification is very expensive. A promising lead to reduce its costs is the use of formal methods. Formal methods are mathematical techniques which allow performing rigorous and high-valued verification tasks during software development. They are already applied in industry. However, the high level of expertise required for their use is a major obstacle for their massive use. In addition to the verification costs issue, today software and their development are subject to an increase in complexity. Model Driven Engineering (MDE) allows dealing with these difficulties by offering models, and tasks to capitalize on these models all along the development lifecycle. The goal of this PhD thesis is to establish a link between formal methods and MDE in order to propose to non-expert users a formal and automatic software verification approach which helps to improve software verification processes. We propose to automatically generate annotations, corresponding to the expected behavioural properties of the software, from the design model to the source code. Then, these annotations can be verified using deductive proof tools in order to ensure that the behaviour of the code conforms to the design model. This PhD thesis takes place in the industrial context of Atos. So, it is necessary to take into account its technical specificities. We use UML for the design modeling, the C language for the software implementation and the Frama-C tool for the proof of this implementation. We also take into account the constraints of the avionics field in which Atos intervenes, and specifically the certification constraints. The contributions of this PhD thesis are the definition of a subset of UML state machine dedicated to the behavioural design of embedded avionics software and in line with current industrial practices, the definition of a C implementation pattern, the definition of generation patterns for the behavioural properties from the design model to the source code and the implementation of the whole approach in a prototype in accordance with the working environment of the potential users associated with Atos. The proposed approach is then assessed with respect to the starting goal of the thesis, to the expectation of the software engineering community and to related work.Lors d'un développement logiciel, et plus particulièrement d'un développement d'applications embarquées avioniques, les activités de vérification représentent un coût élevé. Une des pistes prometteuses pour la réduction de ces coûts est l'utilisation de méthodes formelles. Ces méthodes s'appuient sur des fondements mathématiques et permettent d'effectuer des tâches de vérification à forte valeur ajoutée au cours du développement. Les méthodes formelles sont déjà utilisées dans l'industrie. Cependant, leur difficulté d'appréhension et la nécessité d'expertise pour leur mise en pratique sont un frein à leur utilisation massive. Parallèlement au problème des coûts liés à la vérification logicielle, vient se greffer la complexification des logiciels et du contexte de développement. L'Ingénierie Dirigée par les Modèles (IDM) permet de faire face à ces difficultés en proposant des modèles, ainsi que des activités pour en tirer profit. Le but des travaux présentés dans cette thèse est d'établir un lien entre les méthodes formelles et l'IDM afin de proposer à des utilisateurs non experts une approche de vérification formelle et automatique de programmes susceptible d'améliorer les processus de vérification actuels. Nous proposons de générer automatiquement sur le code source des annotations correspondant aux propriétés comportementales attendues du logiciel, et ce, à partir de son modèle de conception. Ces annotations peuvent ensuite être vérifiées par des outils de preuve déductive, afin de s'assurer que le comportement du code est conforme au modèle. Cette thèse CIFRE s'inscrit dans le cadre industriel d'Atos. Il est donc nécessaire de prendre en compte le contexte technique qui s'y rattache. Ainsi, nous utilisons le standard UML pour la modélisation, le langage C pour l'implémentation et l'outil Frama-C pour la preuve du code. Nous tenons également compte des contraintes du domaine du logiciel avionique dans lequel Atos est impliqué et notamment les contraintes liées à la certification. Les contributions de cette thèse sont la définition d'un sous-ensemble des machines à états UML dédié à la conception comportementale de logiciel avionique et conforme aux pratiques industrielles existantes, la définition d'un patron d'implémentation C, la définition de patrons de génération des propriétés comportementales sur le code à partir du modèle et enfin l'implémentation de l'approche dans un prototype compatible avec l'environnement de travail des utilisateurs potentiels en lien avec Atos. L'approche proposée est finalement évaluée par rapport à l'objectif de départ, par rapport aux attentes de la communauté du génie logiciel et par rapport aux travaux connexes