Accéder directement au contenu Accéder directement à la navigation
Thèse

Intégration des activités de preuve dans le processus de développement de logiciels pour les systèmes embarqués

Résumé : En dépit de l'efficacité des méthodes formelles, en particulier les techniques d'analyse de modèles (model checking), à identifier les violations des exigences dans les modèles de conception, leur utilisation au sein des processus de développement industriel demeure limitée. Ceci est dû principalement à la complexité des modèles manipulés au cours de ces processus (explosion combinatoire) et à la difficulté de produire des représentations formelles afin d'exploiter les outils de vérification existants. Fort de ce constat, mes travaux de thèse contribuent au développement d'un volet méthodologique définissant les activités conduisant à l'obtention des artefacts formels. Ceux-ci sont générés directement à partir des exigences et des modèles de conception manipulés par les ingénieurs dans leurs activités de modélisation. Nos propositions s'appuient sur les travaux d'exploitation des contextes pour réduire la complexité de la vérification formelle, en particulier le langage CDL. Pour cela, nous avons proposé une extension des cas d'utilisation, afin de permettre la description des scénarios d'interaction entre le système et son environnement directement dans le corps des cas d'utilisation. Aussi, nous avons proposé un langage de spécification des exigences basé sur le langage naturel contrôlé pour la formalisation des exigences. Cette formalisation est opérée par transformations de modèle générant des propriétés CDL formalisées directement des exigences textuelles des cahiers des charges ainsi que les contextes CDL à partir des cas d'utilisations étendus. L'approche proposée a été instanciée sur un cas d'étude industriel de taille et de complexité réelles développées par notre partenaire industriel.
Type de document :
Thèse
Liste complète des métadonnées

Littérature citée [97 références]  Voir  Masquer  Télécharger

https://tel.archives-ouvertes.fr/tel-00728431
Contributeur : Bibliothèque Télécom Bretagne <>
Soumis le : jeudi 6 septembre 2012 - 09:33:26
Dernière modification le : mercredi 24 juin 2020 - 16:18:36
Archivage à long terme le : : vendredi 7 décembre 2012 - 03:41:51

Fichier

2012telb0219_Raji_Amine.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : tel-00728431, version 1

Citation

Amine Raji. Intégration des activités de preuve dans le processus de développement de logiciels pour les systèmes embarqués. Génie logiciel [cs.SE]. Télécom Bretagne, Université de Bretagne-Sud, 2012. Français. ⟨tel-00728431⟩

Partager

Métriques

Consultations de la notice

475

Téléchargements de fichiers

583