Soutenance mémoire
Aujourd’hui, les systèmes temps-réel embarqués sont de plus en plus présents dans notre vie quotidienne et fonctionnelle. Il est désormais difficile de trouver un domaine démuni de ces systèmes. Les applications les plus connues des systèmes temps-réel embarqués sont les systèmes de transport (voiture, avion, train) et les systèmes mobiles autonomes (robot, fusé, satellite). De même, les systèmes liés à la gestion d’un périphérique (imprimante, souris sans fil), à la mesure (acquisition en temps réel) et les systèmes domotiques(électroménager) sont des systèmes embarqués pouvant posséder des contraintes temps-réel liées aux capteurs ou actionneurs utilisés. La notion d’embarqué peut être étendue aux objets portables grand public (carte à puce, assistant personnel, téléphone mobile, lecteur, vidéo, consoles de jeu). Le point commun de tous ces systèmes porte la spécificité de leurs contraintes [Js05]. Ces systèmes sont souvent critiques dotés d’un comportement qui est contraint par le temps, dans le sens où ils doivent interagir correctement avec l’environnement non seulement au regard des informations échangées, mais également au regard des instants auxquels ces interactions se produisent.
Actuellement, les systèmes temps-réel embarqués, souvent cachés aux utilisateurs, sont complexes, le risque de les mal concevoir est un problème croissant. Par conséquent, la présence d’un comportement indésirable dans un module ou un logiciel critique peut mener à des conséquences dramatiques, il existe de nombreux exemples de notre vie courante de dysfonctionnements qui avaient entrainé des pertes de vies humaines et des dégâts matériels ou financiers [Pri03, Her01]. Ces dysfonctionnements ont toutes un point en commun : la disproportion entre le coût des dégâts qu’elles ont engendrés et la simplicité des erreurs à la source du problème.
La conception de tels systèmes exige des méthodes et des outils permettant de prendre en compte dans ses phases amont, non seulement les exigences fonctionnelles concernant la correction du calcul mais également les exigences extra-fonctionnelles relatives à l’utilisation optimale de ressources tels que le temps, la mémoire et l’énergie. A ces exigences s’ajoutent celles de l’autonomie, la réactivité et la robustesse. L’objectif d’outils de conception des systèmes temps-réel embarqués est d’aider le concepteur à spécifier, à vérifier rapidement, générer automatiquement des exécutifs conformes à la spécification, et assurer une grande maîtrise de la sûreté de fonctionnement. De ce fait, l’étude de systèmes temps-réel embarqués fait appel à des modèles et des méthodes formelles temporelles et/ou temporisées permettant de répondre aux exigences auxquelles sont soumises de tels systèmes. Ainsi, diverses techniques de spécification et de vérification ont été développées et étendues, offrant donc un ensemble d’outils permettant de garantir le bon fonctionnement du système spécifié.
Modélisation des systèmes temps-réel embarqués
Le développement de systèmes consiste à étudier, concevoir, construire, transformer, mettre au point et maintenir des logiciels. Ces différentes activités qui se situent à plusieurs étapes du cycle de développement, sont plus ou moins facilement réalisées en fonction de méthodes et/ou de langages de modélisation utilisés. Ces derniers permettent notamment de prendre connaissance des attentes de l’usager, créer un modèle « théorique du logiciel », qui servira de plan de construction, puis construire le logiciel, contrôler son bon fonctionnement et son adéquation au besoin. Ceci est aussi valable pour les systèmes embarqués et temps-réel. Cependant, ces derniers ont d’autres caractéristiques et contraintes [Gom84] que l’on ne retrouve pas dans les systèmes logiciels classiques, interaction avec leur environnement, contraintes temps-réel (temps d’exécution, période, etc.), contrôle temps-réel, traitements concurrents, ressources limitées, etc., nécessitent aussi dans leur développement des activités d’analyse des modèles produits avant leur mise en œuvre. Il faut donc utiliser pour leur développement des langages différents et des formalismes variés prenant en compte ces spécificités ou chacune étant adaptée à un métier donné [EL03].
La spécification sert de point de départ à la conception du logiciel. Elle doit donc décrire à un haut niveau d’abstraction les algorithmes, l’architecture matérielle et les contraintes temporelles d’exécution des algorithmes sur l’architecture [KSdeV00]. L’objectif primordial de cette spécification réalisée à l’aide d’un langage de modélisation de haut niveau est d’obtenir un modèle simulable et représentatif de l’implémentation finale de système. Il existe dans la littérature plusieurs langages de modélisation qui ont été développés pour l’analyse et la conception de systèmes temps-réel embarqués, chacun mettant un accent particulier plus sur certains aspects du système que sur d’autres. Le présent chapitre est consacré à l’étude de quelques langages de modélisation, UML, UML-RT, MARTE, AADL et SysML, et nous présentons en détail MARTE, le langage de modélisation ou le profil UML qui est notre choix dans ce travail. Ces derniers langages sont non seulement les plus traités dans la littérature du domaine mais aussi récents et répandus dans le domaine de STRE.
Génie logiciel et ingénierie dirigée par les modèles
Le principal problème du génie logiciel (GL) ne se pose plus en termes de « donnez-moi une spécification immuable et je produis une implantation de qualité », mais plutôt en «comment réaliser une implantation de qualité avec des spécifications continuellement mouvantes» [JGB06]. Quel qu’il soit, un processus de développement logiciel englobe un certain nombre d’activités (comme l’expression des besoins, l’analyse, la conception, l’implantation ou encore la validation) qui chacune produit un ou plusieurs artefacts (documentation, diagrammes, codes sources, fichiers de configuration, fiches de tests, rapports de qualification, etc.). Ces artefacts donnent de multiples points de vue sur le logiciel en cours de développement et, en pratique, sont souvent indépendants les uns des autres. Un problème ici, est d’être capable d’assurer une cohérence entre ces vues, ou au minimum une traçabilité entre les éléments des différents artefacts. L’ingénierie dirigée par les modèles (IDM) y apporte des éléments de réponse.
L’IDM a pour principal objectif de relever un certain nombre de défis du génie logiciel (qualité, productivité, séparation des préoccupations, portabilité, traçabilité, réutilisabilité, maintenabilité, cohérence entre modèles et code, coût, etc.) en suivant une approche à base de modèles dite générative. En focalisant le raisonnement sur les modèles, l’IDM permet de travailler à un niveau d’abstraction élevé, et par la suite de vérifier sur des modèles du système, un ensemble de propriétés que l’on devait vérifier auparavant sur le système final. Avec cette approche, l’IDM permet de lever le verrou consistant à ne pouvoir tester un système que tardivement dans le cycle de vie [DLC10]. L’IDM va également permettre de capitaliser le savoir-faire au niveau des modèles et non pas uniquement au niveau du code source, favorisant ainsi la réutilisabilité, la productivité et la traçabilité. Quelle que soit la technique mise en œuvre pour passer du modèle d’un système à une application logicielle exécutable, il est nécessaire que la sémantique du modèle à exécuter soit clairement définie et surtout non ambigüe. La complétude d’un modèle va influer directement le niveau d’exécution atteignable, par l’une ou l’autre des techniques [JGB06].
Ingénierie dirigée par les modèles pour la conception de systèmes temps-réel embarqués
L’ingénierie du logiciel a considérablement évolué. On a ainsi vu apparaître au fil du temps de nouveaux paradigmes de programmation. On peut notamment citer la programmation fonctionnelle, le paradigme objet et plus récemment les composants et les aspects. Chacune de ces approches vient avec ses avantages et ses inconvénients selon les utilisations, et induit une vision différente de la programmation. Par ailleurs, avec l’augmentation des besoins encouragée par l’amélioration des performances des ordinateurs, la taille des programmes n’a eu de cesse d’augmenter, et le besoin d’outils pour appréhender des grandes quantités de code s’est fait ressentir. Ainsi, des langages avec un plus haut niveau d’abstraction sont apparus, parmi lesquels UML [OMG03]. Le langage UML présente de nombreux diagrammes pour représenter différentes facettes d’un système pendant son développement. Mais il s’est avéré limité, car ne pouvant être totalement en adéquation avec tous les domaines, par exemple l’ingénierie système, les systèmes temps-réel, la robotique, etc. L’Ingénierie Dirigée par les Modèles (IDM) est née de ce besoin de pouvoir créer des langages de modélisation adaptés à chaque situation.
L’IDM ou MDE (Model Driven Engineering) [BB04, Com08], est une discipline qui a pour vocation l’automatisation et la sûreté du développement des systèmes logiciels complexes particulièrement les systèmes embarqués, en fournissant des outils et des langages permettant la transformation de modèles, d’un niveau d’abstraction à un autre ou d’un espace technologique à un autre. C’est un paradigme assez récent de l’ingénierie du logiciel. Son principe essentiel consiste à considérer les modèles comme entités de base dans le développement d’un système, et non plus l’objet comme c’est le cas dans le paradigme objet. De la même manière que le principe tout est objet a permis de faire avancer la technologie objet, le principe tout est modèle est aussi essentiel pour l’ingénierie dirigée par les modèles. Il s’agit de considérer à priori que toute entité manipulée par un système informatique est un modèle. Avec cette technologie les modèles, dont l’utilisation a longtemps été limitée à la documentation des logiciels, font désormais partie de la définition de ces derniers. Ils sont utilisés pour décrire à la fois le problème posé et sa solution. Il existe plusieurs implémentations de l’IDM telles que le MDA (Model Driven Architecture) [Sol00] de l’OMG (Object Management Group), le MIC (Model Integrated Computing) [SK97], les usines à logiciel (SoftwareFactories) [GS04], SNets (Semantic Network) [Béz05a], etc.
Modélisation et méta-modélisation
Un modèle est une abstraction, une simplification d’un système qui est modélisée sous la forme d’un ensemble de faits construits dans une intention particulière. Une définition plus complète est donnée par B. Selic dans [Sel03]. Un modèle doit pouvoir être utilisé pour répondre à des questions sur le système modélisé [Com08]. Les modèles permettent de contenir toute l’information. Il faut que le modèle puisse être représente graphiquement, c’est ce qui le rend facilement accessible et c’est notamment ainsi qu’il peut aider à gérer un système complexe (par rapport à une représentation textuelle). Un méta-modèle est un modèle qui définit le langage d’expression d’un modèle, c’est à dire le langage de modélisation [Poe06]. Il doit être accompagné d’une documentation, écrite en langage naturel. Avec cette documentation, tout ce que l’on peut vouloir exprimer est représentable à l’aide d’un modèle conforme au méta-modèle.
|
Table des matières
1 Introduction Générale
1.1 Introduction
1.2 Problématique
1.3 Contributions
1.4 Plan du manuscrit
I Modèles et outils
2 Modélisation des systèmes temps-réel embarqués
2.1 Introduction
2.2 Génie logiciel et ingénierie dirigée par les modèles
2.3 Ingénierie dirigée par les modèles pour la conception de systèmes temps-réel embarqués
2.3.1 Modélisation et méta-modélisation
2.3.2 Transformation des modèles
2.3.3 Classification des transformations
2.3.4 Approches pour la transformation des modèles
2.4 Langages de modélisation spécifiques aux systèmes temps-réel ou embarqués
2.4.1 UML
2.4.2 UML-RT
2.4.3 MARTE
2.4.4 SysML
2.4.5 AADL
2.5 Discussion
2.5.1 UML
2.5.2 UML-RT
2.5.3 MARTE
2.5.4 SysML
2.5.5 AADL
2.6 Choix de modèle
2.7 Conclusion
3 Modèles formels de temps
3.1 Introduction
3.2 Extensions temporisées des algèbres de processus
3.3 Extensions temporisées des Réseaux de Petri
3.3.1 Réseaux de Petri temporels
3.3.2 Réseaux de Petri temporisés
3.4 Systèmes de transitions étiquetées temporisés
3.4.1 Notions préliminaires
3.4.2 Systèmes de transitions étiquetées
3.4.3 Systèmes de transitions temporisés
3.5 Automates temporisés
3.5.1 Automates de régions
3.5.2 Automates temporisés avec durées d’actions
3.5.2.1 Sémantique de maximalité
3.5.2.2 Spécification des actions avec durées explicites
3.5.2.3 Automate temporisé avec durées d’actions
3.5.3 Autres sous-classes des automates temporisés
3.6 Conclusion
4 Vérification formelle
4.1 Introduction
4.2 Vérification formelle
4.3 Vérification formelle par model-checking
4.3.1 Principe
4.3.2 Méthodes
4.3.3 Outils de vérification
4.3.4 Problème de l’explosion combinatoire
4.4 Vérification formelle basée sur la sémantique de maximalité
4.5 Conclusion
II Contributions
5 Translation des diagrammes de séquence annotés par MARTE en modèles DTPNs
5.1 Introduction
5.2 Approche pour la vérification formelles des spécifications UML MARTE
5.3 Formalisation des diagrammes de séquence annotés par le profil MARTE
5.4 Translation des diagrammes de séquence UML MARTE en modèle DTPNs
5.4.1 Constructions de base
5.4.1.1 Transmission Inter-objets
5.4.1.2 Transmission intra-objets
5.4.2 Fragments combinés
5.4.2.1 Fragment Seq
5.4.2.2 Fragment Strict
5.4.2.3 Fragment Par
5.4.2.4 Fragment Alt
5.4.2.5 Fragment Opt
5.4.2.6 Fragment Loop
5.5 Conclusion
6.1 Introduction
6.2 Système de contrôle d’ascenseur
6.2.1 Architecture globale
6.2.2 Description
6.3 Modélisation
6.4 Vérification par model-checking
6.5 Conclusion
7 Travaux connexes et discussion
7.1 Travaux connexes
7.2 Discussion
7.3 Conclusion
8 Conclusion générale et perspectives
Liste des publications
Liste des acronymes
Bibliographique
