Soutenance mémoire
Langages de modélisation
LANGAGES DE MODELISATION
Les langages de modélisation sont couramment utilis ´es pour spécifier, visualiser, stocker, documenter, et ´echanger des mod`eles de conception. Ils sont sp´ecifiques au domaine et contiennent toutes les informations syntaxiques, s´emantiques et de pr ´esentation concernant une application donn´ee dans un domaine. Diff ´erents langages de modélisation ont ét ´e d´efinis par des organisations et des entreprises afin de cibler diff ´erents domaines tels que le d´eveloppement web (WebML [20]), t él ´ecommunications (TeD [2]), matériel (HDL [1]), logiciels, et plus r ´ecemment, les syst `emes (UML [14]). D’autres langages tels que IDEF [19] ont ét ´e conc¸us pour un large ´eventail d’utilisations, y compris la modélisation fonctionnelle, la modélisation des donn´ees et la modélisation de r ´esaux. Bien que l’ing énierie des syst `emes existe depuis plus de cinq d´ecennies, jusqu’ `a r ´ecemment, il n’y avait pas de langage de modélisation dédi ´e `a cette discipline. Traditionnellement, les ing ´enieurs syst `emes ont beaucoup travaill ´e sur la documentation pour exprimer les exigences syst `eme et, en l’absence d’une langue standard sp´ecifique, ont utilis ´e diff ´erents langages de modélisation pour exprimer une solution de conception compl`ete. Cette diversit ´e de techniques et d’approches a limit ´e le travail coopératif et l’ ´echange d’information. Parmi les langages de modélisation existants qui ont ét ´e utilis ´es par les syst `emes ing ´enieurs, on peut citer HDL, IDEF et EFFBD.
Afin de fournir une solution `a ce probl `eme, OMG et INCOSE [10], avec un certain nombre d’experts dans le domaine de l’ing énierie syst `eme, ont collabor ´e pour la construction d’un langage de modélisation standard. UML, étant le langage de modélisation par excellence pour l’ing énierie logicielle, était le langage de choix destin´e `a la personnalisation `a l’ ´egard des besoins des ing ´enieurs syst `emes. Cependant, la version UML 1.x s’est r ´evél ´ee inad´equate pour une telle utilisation et donc la r évision en ´evolution de UML (c’est- ` a-dire, UML 2.0) a ét ´e publi ´ee, avec des fonctionnalit ´es spéciales pour les ing ´enieurs syst `emes. En avril 2006, une proposition pour un langage de modélisation standard pour la modélisation des syst `emes, `a savoir SysML [11], a ét ´e soumis `a l’OMG, avec l’objectif d’aboutir `a un processus de normalisation final [24].
LA RELATION ENTRE UML ET SYSML SysML r éutilise un sous-ensemble de UML 2.1 [15], appel´e ”UML4SysML”, qui repr ´esente environ la moiti ´e du langage UML. Une partie importante de l’UML des concepts ont ét ´e ´ecart ´es car ils n’ étaient pas considér ´es comme pertinents pour les besoins du mod` ele de SE. Certains des diagrammes r éutilis ´es ont ét ´e inclus comme dans UML 2.1.1 [15]. Ceux-ci incluent la machine d’ état, la s´equence et les diagrammes de cas d’utilisation. D’autres diagrammes ont ét ´e ´etendus, tels que les diagrammes d’activit é, afin de r ´epondre aux besoins sp´ecifiques des SE. De plus, SysML a omis certains diagrammes UML, `a savoir d’objet, de composant, de d´eploiement,de communication, de temps et d’interactions. Les diagrammes de structure dont diagramme de Classe et composition ont ét ´e fondamentalement modifi´es et remplac´es par des diagrammes de définition de blocs et diagrammes de blocs internes. Ces extensions sont bas´ees sur le m´ecanisme de profilage UML standard, qui inclut les st ér ´eotypes UML, extensions de diagramme UML et la biblioth `eques de mod`eles. Le m´ecanisme de profilage a ét ´e choisi sur d’autres m´ecanismes d’extension afin de tirer parti des outils existants bas´es sur UML pour la modélisation de syst `emes. En outre, SysML ajoute deux nouveaux diagrammes, ceux-ci étant diagrammes d’exigences et diagrammes paramétriques, et int `egre de nouvelles capacit´es de spécification liens tels que l’allocation. La relation entre UML et SysML est illustr ´ee dans 2.4.
ING´ENIERIE DIRIG´EE PAR LES MODELES – IDM L’ing enierie dirigee par les mod`eles (IDM), ou Model Driven Engineering (MDE) en anglais, a permis plusieurs améliorations significatives dans le d´eveloppement de syst `emes complexes en permettant de se concentrer sur une pr ´eoccupation plus abstraite que la programmation classique. Il s’agit d’une forme d’ing énierie g´enérative dans laquelle tout ou partie d’une application est engendr´ee `a partir de mod`eles. Un mod` ele est une abstraction, une simplification d’un syst`eme qui est suffisante pour comprendre le syst `eme modélis ´e et r ´epondre aux questions que l’on se pose sur lui. Un syst `eme peut ˆ etre d´ecrit par diff ´erents mod`eles li ´es les uns aux autres. L’id ´ee phare est d’utiliser autant de langages de modélisation diff ´erents (Domain Specific Modeling Languages – DSML) que les aspects chronologiques ou technologiques du d´eveloppement du syst `eme le nécessitent. La définition de ces DSML, appel´ee m´etamodélisation, est donc une probl ´ematique cl ´e de cette nouvelle ing énierie. Par ailleurs, afin de rendre opérationnels les mod`eles (pour la g´enération de code, de documentation et de test, la validation, la vérification, l’exécution, etc.), une autre probl ´ematique cl ´e est celle de la transformation de mod` ele. En r ´esumé, IDM couvre le cycle de vie complet de l’application , elle est bas´ee sur deux principaux concepts : la m´etamodélisation et la transformation de mod`eles qui sont toujours des domaines de recherche [27].
M´ETHODES FORMELLES (V´ERIFICATION)
La verification formelle est un processus qui permet de prouver qu’un syst `eme se comporterait en parfait accord avec sa spécification. Cela revient `a utiliser des approches mathematiques qui permettent de montrer que l’impl ´ementation satisfait la spécification. Dans ce cas une considération de tous les cas possibles est implicite. Ces derni `eres ann´ees, les m´ethodes formelles ne sont plus uniquement des th `emes de recherche, mais plut ˆ ot un concurrent potentiel, si ce n’est pas une solution de remplacement, de la vérification par simulation. Ces points de vue partent d’une correcte ´enumération des caract éristiques des m´ethodes formelles. Les avantages des m´ethodes de vérification formelle compar´ees `a la vérification par simulation sont nombreux. En effet, ces m´ethodes consid`erent toutes les entr ´ees possibles au syst `eme, vérifient la validit ´e des propri ét ´es du syst `eme math´ematiquement, ne n´ecessitent pas une spécification des sorties du syst`eme pr ´evue de plus elles permettent, pour certains outils, d’identifier les traces des erreurs s’il y a lieu. La vérification formelle poss`ede, elle aussi, certains inconv´enients. En effet, elle demande un effort suppl´ementaire pour parvenir `a une description compl`ete et simple du syst `eme `a vérifier. C’est qu’il est n´ecessaire de définir une spécification, d’une part, tenant en considération tous les détails du syst `eme, et d’autre part, assez simple `a manipuler dans la phase de vérification. D’autre part c’est difficile de faire un raffinement sans perte des propri ét ´es du syst `eme.
CONCLUSION
Le diagramme de s´equence SysML a les merites d’une visualisation plus elevee et une meilleure lisibilit é, tandis que le mod` ele d’automates poss`ede les mérites d’une définition plus stricte et d’une meilleure vérifiabilit é. Combinant les forces complementaires des deux mod`eles, notre projet propose ainsi une approche de vérification formelle impl´ement´ee dans un plug-in appel´e Formal-Sequence. Tout d’abord, les diagrammes de s´equence sont simplifi ´es et formellement d´efinis dans un diagramme bidimensionnel appel´e S D2D. Ensuite, un ensemble de r `egles de transformation est ´etabli entre S D2D et le r ´eseau d’automates temporis ´es (TANe). Enfin, sur la base des relations de mappage, la transformation des S D2D `a TANe est ´etablie. Une vérification formelle peut ensuite ˆ etre effectu´ee pour vérifier les propri ét ´es sp´ecifiques au domaine `a l’aide de vérificateurs de mod`eles automatis´es tels que UPPAAL.
Notre approche comble le foss´e entre la modélisation semi-formelle et la modélisation formelle des comportements logiciels. Les r ésultats que nous avons obtenus montrent que l’approche propos´ee est satisfaisante et prometteuse. Il est int ´eressant de noter que plusieurs travaux antérieurs ont déj `a tent ´e de formaliser [36, 32] et de vérifier [26, 30] des diagrammes de s´equence. Ces travaux tentent de combiner le diagramme de s´equence (semi-formel) avec les techniques formelles (comme les r ´eseaux de Petri [37, 34], les automates [33] et d’autres techniques formelles [21, 23]), qui int `egrent les mérites de la modélisation semi-formelle et de la modélisation formelle et comble le foss´e entre eux. La majorit ´e des approches propos´ees se concentrent d’abord sur la transformation du diagramme de s´equence en un mod` ele formel, puis utilisent un vérificateur de mod` ele automatis´e pour simuler et vérifier les propri ét ´es ´ecrites sous forme d’une logique lin éaire temporelle (LTL).
|
Table des matières
1 Introduction
1.1 Contexte
1.2 Probl ´ematique
1.3 Objectifs
1.4 Organisation du m´emoire
2 Etat de l’art
2.1 Langages de modélisation
2.1.1 UML
2.1.1.1 Architecture UML
2.1.1.2 Profil UML
2.1.2 SysML
2.1.2.1 Architecture SysML
2.1.2.2 Les quatre piliers de SysML . .
2.1.2.3 La relation entre UML et SysML .
2.1.2.4 Diagramme de S´equence
2.1.3 Automates temporis ´es
2.2 Ingénierie dirig ´ee par les mod`eles – IDM
2.2.1 Définitions
2.2.2 La m´etamodélisation
2.2.3 Transformation de mod`eles
2.2.3.1 Pourquoi la transformation de mod`eles
2.2.3.2 Approches de transformation de mod`eles
2.2.3.3 Transformation Model to Text – M2T
2.2.3.4 Transformation Model to Model – M2M
2.3 Verification et Validation
2.3.1 Test et Simulation (Validation)
2.3.2 M´ethodes Formelles (Vérification)
2.3.2.1 Model-checking
2.3.2.2 Theorem Proving
3 Vers une Verification Formelle des Mod`eles SysML
3.1 Vue generale de notre approche
3.2 Des diagrammes de s´equence aux automates temporis ´es
3.2.1 Diagramme de S´equence Simplifi´e S D2D
3.2.1.1 Syntaxe du Diagramme de S´equence S D2D
3.2.1.2 S´emantique de Diagramme de s´equence .
3.2.2 Automate Temporiseé´ tendu TANE
3.2.3 Syntaxe et Définition de TANE
3.2.4 Automate Temporis ´e et Model Checker
3.3 R`egles de transformation de S D2D
3.4 Simulation et Vérification par TANE
3.4.1 Simulation
3.4.2 Vérification formelle
4 Formal-Sequence : un Plug-in Generation d’automates
4.1 De SysML vers UPPAAL
4.2 Algorithmes d´evelopp´es
4.2.1 Extraction des donn´ees
4.2.2 Construction de TANE
4.3 E´ tude de cas
4.3.1 Description du syst `eme ATM
4.3.2 Modélisation du comportement de l’ATM
4.3.3 Modélisation formelle de l’ATM
4.3.4 Vérification de l’ATM
4.3.4.1 Simulation avec l’outil Uppaal .
4.3.4.2 Vérification avec l’outil Uppaal .
5 Conclusion Generale
5.1 Conclusion
5.2 Perspectives
Télécharger le rapport complet
