Integrating Formal Verification Techniques into Software Development Process for Embedded Systems

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

Amine Raji (1)

1 LUSSI - Département Logique des Usages, Sciences sociales et Sciences de l'Information

In past years, formal verification techniques and tools were widely developed and used by the research community. However, the use of formal verification at industrial scale remains difficult, expensive and requires lot of time. This is due to the size and the complexity of manipulated models, but also, to the important gap between requirement models manipulated by different stackholders and formal models required by existing verification tools. This dissertation aims therefore to develop a methodology that define activities that fill this gap by generating formal artifacts from textual requirements and existing design models. Our approach is based on previous work on the exploitation of contexts for formal verification, particularly, CDL language. We extended UML use cases with the ability to precisely describe interaction scenarios between the system under validation and its context. We also defined a requirement specification language based on the processing of natural language to formalize textual requirements. This formalization is performed thanks to model transformations that generate CDL properties from textual requirements and CDL context models form extended use cases scenarios. The proposed methodology is instantiated on a reel industrial case study provided by our industrial partner.

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.

Mots clés: Formal verification; Context-aware verification; Requirements engineering; Software development process; User Context Models

Mots clés: Vérification formelle; Exploitation du contexte; Ingénierie des exigences; Model-Checking; Processus de développement; Context Description Language; Users Context Models; Observer-Based Prover

Domaines: Génie logiciel [cs.SE]

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. ⟨NNT : ⟩. ⟨tel-00728431⟩