Développement d'applications logicielles sûres de fonctionnement: une approche dirigee par la conception

• Main Author: Enard, Quentin
• Language: FRE
• Published: Université Sciences et Technologies - Bordeaux I 2013
• Subjects: [INFO:INFO_SE] Computer Science/Software Engineering; Développement Logiciel; Langage de Conception; Génération de Code; Sûreté de Fonctionnement
• Online Access: http://tel.archives-ouvertes.fr/tel-00839298; http://tel.archives-ouvertes.fr/docs/00/83/92/98/PDF/these_tel.pdf

Dans de nombreux domaines tels que l'avionique, la médecine ou la domotique, les applications logicielles jouent un rôle de plus en plus important, allant jusqu'à être critique pour leur environnement. Afin de pouvoir faire confiance à ces applications, leur développement est contraint par des exigences de sûreté de fonctionnement. En effet il est nécessaire de démontrer que ces exigences de haut-niveau sont prises en compte tout au long du cycle de développement et que des solutions concrètes sont mises en oeuvre pour parvenir à les respecter. De telles contraintes rendent le développement d'applications sûres de fonctionnement particulièrement complexe et difficile. Faciliter ce processus appelle à la recherche de nouvelles approches de développement qui intègrent des concepts de sûreté de fonctionnement et guident les développeurs lors de chacune des étapes nécessaires à la production d'une nouvelle application digne de confiance. Cette thèse propose ainsi de s'appuyer sur une approche dirigée par la conception pour guider le développement des applications sûres de fonctionnement. Cette approche est concrétisée à travers une suite d'outils nommée DiaSuite et offre du support dédié à chaque étape du développement. En particulier, un langage de conception permet de décrire à la fois les aspects fonctionnels et non-fonctionnels des applications en se basant sur un paradigme dédié et en intégrant des concepts de sûreté de fonctionnement tels que le traitement des erreurs. A partir de la description d'une application, du support est généré pour guider les phases d'implémentation et de vérification. En effet, la génération d'un framework de programmation dédié permet de guider l'implémentation tandis que la génération d'un modèle formel permet de guider la vérification statique de l'application et qu'un support de simulation permet de faciliter les tests. Cette approche est évaluée grâce à des cas d'études réalisés dans les domaines de l'avionique et de l'informatique ubiquitaire.