Soutenance mémoire
Les méthodes formelles
Les méthodes formelles ont contribué, depuis plusieurs années, à l’apport de solutions rigoureuses et puissantes pour aider les concepteurs à produire des systèmes non défaillants. Dans ce domaine, les techniques de model-checking [Queille & Sifakis 1982, Clarke et al. 1986] ont été fortement popularisées grâce à leur faculté d’exécuter automatiquement des preuves de propriétés sur des modèles logiciels. Elles permettent de confronter un modèle de conception aux propriétés à vérifier et ainsi détecter les erreurs de conception. Ces techniques de vérification peuvent être automatiques (presse-bouton) et connaissent un succès grandissant dans l’industrie depuis plusieurs années. Le principe consiste à construire, à partir du modèle du logiciel à valider, l’espace des états atteignables puis, en parcourant l’ensemble de ces états, à vérifier le respect des propriétés comportementales et ainsi que les contraintes temporelles attendues du système.
De nombreux outils (model-checkers) mettant en œuvre cette technique ont été développés [Holzmann 1997, Larsen et al. 1997, Berthomieu et al. 2004, Fernandez et al. 1996, Cimatti et al. 2000]. Malgré leur performance croissante, leur utilisation en contexte industriel reste encore difficile. Leur intégration dans un processus d’ingénierie industriel est alors encore faible comparativement à l’énorme besoin de fiabilité dans les systèmes critiques. Cette contradiction trouve en partie ses causes dans la difficulté réelle de mettre en œuvre des concepts théoriques dans un contexte industriel. Une première difficulté liée à l’utilisation de ces techniques de vérification provient du problème bien identifié de l’explosion combinatoire du nombre de comportements des modèles, induite par la complexité interne du logiciel qui doit être vérifié. Cela est particulièrement vrai dans le cas des systèmes embarqués temps réel, qui interagissent avec des environnements impliquant un grand nombre d’entités. Beaucoup de travaux en méthodes formelles ont été menés afin de maîtriser l’explosion combinatoire [Mc.Millan & Probst 1992, Peled 1998, E.A. Emerson and S. Jha and D. Peled 1997, Alur et al. 1997, Valmari 1991, Godefroid et al. 1996, Bosnacki & Holzmann 2005, Park & Kwon 2006]. Des techniques développées autour du model-checking consistent en général à diminuer l’espace d’états du système global de telle manière à pouvoir effectuer une recherche d’accessibilité d’états.
Une autre difficulté est liée à l’expression formelle des propriétés nécessaires à leur vérification. Les artefacts produits à travers les activités du processus de développement industriel (exigences, spécification, modèles de conception) ne sont pas directement exploitables pour l’utilisation des outils de vérification. En effet, les exigences sont disponibles sous une forme textuelle qui les rendent inexploitables sans une réécriture préalable (formalisation) [Lu et al. 2008]. Traditionnellement, le model-checking implique de pouvoir exprimer les exigences à l’aide de formalismes de type logique temporelle comme LTL [Pnueli 1977] ou CTL [Clarke et al. 1986]. Bien que ces langages aient une grande expressivité, il n’est pas aisé de les utiliser systématiquement pour la spécification de modèles de taille industrielle afin de pouvoir valider ces derniers. L’approche, dans laquelle s’insère ce travail, prend un point de vue complémentaire, par rapport aux techniques décrites précédemment, en considérant la réduction non plus du système mais plutôt de son environnement.
L’approche OBP
Partant des constats précédents, des travaux [Roger 2006, Dhaussy & Boniol 2007, Dhaussy et al. 2009, Dhaussy et al. 2011] se sont penchés sur cette problématique en cherchant à faciliter l’utilisation des outils de model-checking. Les objectifs visés étaient d’étudier les conditions et les techniques permettant à un ingénieur en charge de vérifier des exigences sur un modèle logiciel dans un contexte industriel. La contribution voulait être un apport pour permettre d’exprimer facilement des exigences sous une forme compréhensible par un non expert des logiques temporelles et de pouvoir mener des vérifications par model-checking sur des modèles de grande taille. L’idée suivie, pour contourner l’explosion combinatoire lors des explorations des modèles, est, d’une part, de chercher à réduire les comportements des modèles lors de leur exploration en considérant leur environnement. La réduction est basée sur une description de cas d’utilisation particuliers de l’environnement, nommés contextes avec lequel le système interagit. L’objectif est de guider le model-checker à concentrer ses efforts non plus sur l’exploration d’un automate global mais sur une restriction pertinente de ce dernier pour la vérification de propriétés spécifiques. D’autre part, un langage à base de patrons de définition de propriété a été défini pour faciliter l’expression des exigences. La description des contextes et des propriétés est intégrée dans un même langage nommé CDL (Context Description Language) et exploité par l’outil OBP (Observer-Based Prover) [Dhaussy et al. 2009].
LIMITES DE L’APPROCHE OBP/CDL
Suite aux expérimentations menées avec l’approche OBP/CDL, nous dressons un bilan et identifions les difficultés de mise en œuvre de celle-ci. Nous nous proposons ensuite d’étendre les travaux précédents pour contribuer à apporter des améliorations. Lors des expérimentations, les diagrammes de contexte ont été construits par des ingénieurs eux-même en collaboration avec l’équipe qui a proposé CDL. Cette construction s’est effectuée d’une part, à partir de scénarios décrits dans les documents de conception et, d’autre part, à partir des documents d’exigences. Deux difficultés majeures sont alors apparues. La première est le manque de description complète et cohérente du comportement de l’environnement des modèles analysés.
Par exemple, des données concernant les modes d’interaction peuvent être implicites. Le développement des diagrammes CDL requiert alors beaucoup de discussions avec les experts qui ont conçu les modèles afin d’expliciter toutes les hypothèses associées aux contextes. La deuxième difficulté concerne la compréhension des exigences et leur formalisation en propriétés formelles. Celles-ci sont regroupées dans des documents de niveaux d’abstraction différents, correspondants aux exigences système ou dérivées. L’ensemble des exigences analysées était rédigé sous forme textuelle. Certaines d’entre elles donnaient lieu à plusieurs interprétations différentes. D’autres faisaient appel à une connaissance implicite du contexte dans lequel elles doivent être prises en compte.
Il nous apparaît donc nécessaire de pouvoir offrir à l’utilisateur des moyens simples à mettre en œuvre permettant de spécifier de manière cohérente et complète les contextes ainsi que les exigences à vérifier. Le but recherché est que l’utilisateur puisse construire un ensemble d’artefacts nécessaires et suffisants pour produire automatiquement les modèles CDL.
Difficulté liée à l’expression des contextes et des exigences
Dans le but d’éviter l’explosion combinatoire lors de la vérification avec l’approche OBP/CDL, il est nécessaire de pouvoir identifier une multitude de contextes suffisamment restrictifs pour limiter le nombre de comportements du modèle lors de l’exploration. Ceci implique une description d’un ensemble de contextes qui décrivent de manière complète les scénarios d’utilisation du système. Toutefois, le langage CDL est considéré par les industriels comme étant de plus bas niveau. En effet, un modèle CDL référence des opérations de communication, en terme d’entrée et sortie de messages, dotés parfois de nombreux paramètres. Construire un modèle CDL revient donc à identifier l’ensemble des acteurs interagissant avec le système dans un contexte particulier, puis tous les événements échangés ainsi que leurs enchaînements. La construction de tels modèles n’est donc pas une tâche facile. Les cas d’utilisations, fournis par les partenaires, sont généralement décrits en langage naturel, sous la forme de diagrammes d’activités ou de diagrammes de séquences. Ils décrivent les interactions entre les composants du système et les entités de l’environnement. Chaque diagramme, décrivant un cas d’utilisation référence plusieurs acteurs. Un modèle CDL formalise, quant à lui, le contexte en décrivant séparément le comportement de chaque acteurs. Aujourd’hui, la formalisation des interactions, décrits dans les cas utilisation, sous forme de modèles CDL est un processus manuel qui nécessite un effort important pour faire le lien entre ces deux niveaux de modélisation (Cas d’utilisation et CDL), en plus d’une bonne connaissance de la syntaxe et la sémantique de CDL. Il y a donc un fossé entre les descriptions fournies par les cahiers de charges et les documents de spécification et les modèles CDL (Figure 1.1). Ceci est dû à l’écart sémantique entre les descriptions textuelles des uses cases, décrivant les scénarios et les modèles CDLs qui capturent les échanges de messages émis ou reçus par chaque acteur.
Par ailleurs, l’expression de exigences pose également certaines difficultés. En effet, les exigences exprimées dans les cahiers des charges sont décrites en langage naturel. Elles référencent des conditions liées au comportement du modèle, le comportement spécifique (un mode) du système, ainsi que les évènements dont certains n’étant pas toujours observables. Dans le langage CDL, les patrons de spécification de propriétés permettent de décrire les propriétés en terme de détection d’évènements (envois et réceptions de messages), de prédicats constituant les champs de vérification des propriétés (les Scopes) [Konrad & Cheng 2005a]). Là aussi, le passage entre les exigences textuelles et le ou les patrons à utiliser nécessite un effort important de réécriture.
Définition d’une méthodologie de vérification avec CDL
Toujours dans l’objectif d’aider l’utilisateur dans sa construction des modèles CDL. Il est nécessaire d’identifier clairement les étapes de cette activité. En effet, les modèles manipulés par celui-ci en phase de conception doivent pouvoir être exploités pour générer automatiquement les modèles CDL. Dans ce contexte, nous ne prétendons pas apporter de solutions pour assurer la complétude de l’ensemble des cas d’utilisation que l’utilisateur identifie et formalise. Ceci ferait l’objet d’un travail spécifique. Mais nous cherchons à proposer un type de structure de données rassemblant l’ensemble des données nécessaires à la génération des modèles CDL.
|
Table des matières
Introduction et Bibliographie
1 Introduction générale
1.1 Contexte de travail
1.1.1 Recherche de fiabilité des systèmes embarqués
1.1.2 Les méthodes formelles
1.1.3 L’approche OBP
1.2 Limites de l’approche OBP/CDL
1.2.1 Difficulté liée à l’expression des contextes et des exigences
1.2.2 Définition d’une méthodologie de vérification avec CDL
1.3 Objectif de la thèse
1.4 Organisation du mémoire
2 Etat de l’art
2.1 Capture et formalisation des entités du domaine
2.1.1 Méthodologie d’analyse et de conception orientée-objet
2.2 Les contextes
2.2.1 Intérêt de la formalisation des contextes pour la vérification formelle
2.2.2 Etat de l’art sur la capture et la formalisation des contextes
2.3 L’ingénierie des exigences
2.3.1 Capture, évolution et raffinement des exigences
2.3.2 Langages de modélisation des exigences
2.3.3 Langage naturel contraint
2.3.4 Patrons de propriétés
2.4 Les méthodologies de développement
2.4.1 Processus de développement
2.4.2 Processus de vérification formelle des exigences en contexte industriel
2.5 Discussion et synthèse
3 La méthodologie CDL et l’outillage OBP
3.1 Présentation du cas d’étude
3.1.1 Le système contrôleur SM
3.1.2 Architecture du système
3.1.3 Cas d’utilisation
3.1.4 Exemple d’exigence à vérifier sur le modèle
3.2 Les principes mis en œuvre de la vérification avec CDL
3.2.1 Prise en compte de l’environnement des modèles à valider
3.2.2 Identification des contextes pour contourner l’explosion combinatoire
3.2.3 Spécification des propriétés
3.2.4 Les bénéfices de l’approche
3.3 Le langage CDL
3.3.1 Description hiérarchique du contexte
3.3.2 Syntaxe formelle de CDL
3.4 L’outillage OBP
3.4.1 Transformation des modèles CDL
3.4.2 Partitionnement automatique des graphes de contexte
3.5 La méthodologie OBP
3.5.1 Le processus de vérification
3.6 Discussion et synthèse
4 Spécification du domaine
4.1 Construction d’une terminologie
4.1.1 Spécification du domaine
4.1.2 Représentation du vocabulaire du domaine
4.2 Modèle conceptuel pour la spécification du domaine
4.2.1 DomainElements package
4.2.2 Terminology Package
4.3 Discussion et synthèse
5 Capture et Formalisation des Contextes
Conclusion
Télécharger le rapport complet
