IDL

Ingénierie Du Logiciel

  • Full Screen
  • Wide Screen
  • Narrow Screen
  • Increase font size
  • Default font size
  • Decrease font size

Séminaire IDL 14/03/2012

Envoyer Imprimer

Intervenant : Amine Raji, Doctorant, ENSTA Bretagne.

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

Date & Lieu : 14 Mars 2012, 14h-16h, salle 117-A, 1er étage, Bâtiment LC, site AES, UBO.
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, les travaux exposés dans ce travail de thèse contribuent au développement d'un volet méthodologique définissant les activités conduisant à l'obtention des artéfacts 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 UML, 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. Nous avons aussi 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é par notre partenaire industriel.

You are here: