DÉFINITION ET FORMALISATION D’UNE MÉTHODOLOGIE 

Le mot méthodologie utilisé dans ce chapitre correspond à la description d’une succession d’activités de travail qui gouvernent la production de modèles formels assimilables par les outils existants de vérification [Colombo et al. 2007]. Pour ce qui est du processus de développement, celui-ci correspond aux activités mises en oeuvre au sein d’une équipe de développement pour la production de biens livrables. Ces biens livrables correspondent aux modèles de conception que l’on désire valider formellement afin de s’assurer du respect des exigences exprimées au début du cycle de développement. 

Vue d’ensemble de la méthodologie 

La méthodologie que nous proposons dans cette thèse intègre les activités liées à la vérification formelle des modèles de conception. En ce sens, elle raffine les méthodologies de conception existantes pour y intégrer les préoccupations de formalisation et de génération de code formel. Le but étant de pouvoir utiliser les outils de vérification formelle existants tout au long du processus de développement. L’approche que nous proposons dans cette thèse a été définie de manière générique pour s’appliquer aux principaux processus de développement utiliser dans le contexte du développement de système logiciels embarqués. En effet, nous avons présenté dans la section 2.4 deux des processus de développement les plus répandus dans ce contexte : le processus unifié UP [Booch et al. 1999] et le processus de développement en « V ». À partir de ces deux processus, nous avons dégagé les activités de développement communes afin d’y intégrer les activités proposées dans notre approche. Ces activités sont : (1) le traitement des exigences (2) Spécification des cas d’utilisation (3) l’analyse et (4) la validation.• Le traitement des exigences: cette activité concerne la formalisation des données d’entrées à l’aide des langages proposés dans la deuxième partie de ce mémoire, • La spécification des cas d’utilisation: permet de formaliser les scénarios d’interaction entre le composant du système à vérifier et son contexte, • L’analyse: consiste en la génération de modèles CDL à partir des modèles utilisateurs produits par la phase de traitement des exigences, • La vérification: concerne l’exploitation des outils de vérification formelle pour obtenir le résultat. Ainsi, la figure 8.1 présente la méthodologie proposée et l’organisation des activités de vérification proposée selon les activités des processus de développement. Le point conception préliminaire du système étudié. Ces modèles regroupent les diagrammes de cas d’utilisation et de séquences qu’on trouve dans les documents de spécification pour illustrer et clarifier les exigences sur les fonctionnalités attendues du système. Pour que le modèle à vérifier soit exploité par la méthodologie proposée, celui-ci doit être décrit par un langage formel exploitable par l’outil de vérification formel utilisé. Dans le cas de notre travail, le modèle à validé est présenté sous la forme d’un programme FIACRE pour être vérifier par l’outil TINA. L’aspect formalisation du modèle du système à vérifier n’entre pas dans le périmètre de nos travaux, menés dans le cadre de cette thèse. Dans la suite de ce chapitre, nous allons détailler chacune des quatre activités méthodologiques. Mais avant de procéder, nous allons présenter la notation de description de méthodologie utilisée dans la section qui suit. 

Notation utilisée pour la description de la méthodologie 

La notation utilisée dans ce chapitre pour décrire un processus de développement méthodologique étend les diagrammes d’activités UML2 [OMG 2007]. Nous reprenons la syntaxe concrète utilisée dans [Fontan 2008] pour décrire notre méthodologie. En effet, dans ce dernier, les étapes méthodologiques sont décrites par des activités qui peuvent être raffinées en sous activités. Un diagramme d’activité commence obligatoirement par un disque noir représentant le début de la première activité. Chaque étape est reliée par une flèche de transition montrant les relations de précédence entre les activités. Une activité peut être décomposée en sous activités. La figure 8.2 montre un exemple de processus de développement méthodologique. ors des étapes de la méthodologie, des artefacts peuvent être produits, consommés ou modifiés par une ou plusieurs étapes. La production (création/modification) et la consommation (consultation) sont respectivement représentées par des flèches pleines (par opposition aux flèches de transition entre activités) sortantes et entrantes de l’activité sur les côtés. Les artefacts modifiés lors d’une activité méthodologique sont représentés par une flèche sortante marquée en trait discontinu. Un artefact sortant est disponible pour toutes les autres activités, contrairement à la production d’un artefact qui n’est autorisé qu’à l’intérieur des activités qui possèdent une flèche sortante. Le diagramme d’activités représentant la méthodologie est ainsi composé d’étapes méthodologiques, de référence vers les artefacts utilisés par ces activités et de flèches reliant ces derniers. Ainsi, la méthodologie proposée définit un ensemble d’activités méthodologiques et associe à chacune de ces étapes la livraison d’artefacts. La notion d’artefact ici fait référence à des modèles conformes à des métamodèles.

 APPLICATION À LA VÉRIFICATION FORMELLE DES EXIGENCES ET L’EXPLOITATION DES CONTEXTES 

La méthodologie proposée est dédiée à la vérification formelle de modèles et ne couvre donc pas les phases de conception et d’implémentations. Le but de celle-ci est d’intégrer la production de modèles formels nécessaires à l’utilisation des outils existants de model checking. Comme nous l’avons précisé précédemment, nous nous plaçons dans le cadre de la vérification par exploitation de contextes, et notamment en utilisant des modèles CDL ainsi que la chaine d’outils OBP développés dans le laboratoire. 

Traitement des exigences

 Dans notre approche, la première activité est l’étude des documents d’exigences par l’expert métier afin de les réécrire sous la forme d’exigences URM. Nous supposons que les exigences définies dans ces documents, fournis par le client, sont des exigences de bas niveau (par opposition aux objectifs de haut niveau). En effet, chaque exigence devra porter sur une fonctionnalité simple du système étudié afin de vérifier des contraintes telles que le séquencement d’événements ou des contraintes temporelles sur les messages échangés. Comme nous l’avons préciser au par avant, la décomposition des exigences étant une problématique à part entière, elle n’entre pas dans le cadre de cette thèse. La figure 8.3 illustre l’activité méthodologique de la phase de traitement des exigences. 

Spécification des cas d’utilisation 

Cette activité concerne l’exploitation des documents de spécification afin d’identifier les différents cas d’utilisation du système. Ces cas d’utilisation sont ensuite détaillés afin de spécifier les scénarios d’interaction entre le système et les entités de son environnement (acteurs). À ce stade, les scénarios d’interactions peuvent ne référencer que les séquences d’échange nominal entre le système et le contexte. L’information permettant de spécifier de tels scénarios est généralement définie dans les cahiers de charge. Par la suite, ces scénarios peuvent être raffinés afin d’y intégrer les différentes exceptions potentielles qui peuvent altérer le déroulement du scénario nominal. Selon les exceptions identifiées, des handlers peuvent être définis pour enrichir la spécification du scénario principal.