La validation temporelle des systèmes temps réel est nécessaire dans le cadre d’applications critiques tels l’aéronautique, le spatial ou l’automobile. Il s’agit, dans ces systèmes, de garantir les temps de réponse des tâches ainsi que le déterminisme de leurs communications. En raison de la complexité des systèmes actuels ainsi que de leur criticité, il est nécessaire de mettre en place une démarche de conception réduisant le temps de développement et ainsi le temps de mise en marché (time-to-market), tout en réduisant les risques d’erreurs de conception.Ce contexte rend l’ingénierie dirigée par les modèles particulièrement adaptée au développement de ce type de système. Les contributions de cette thèse partent des constats suivants. Premièrement, malgré la multitude des modèles d’analyses existants les modèles actuels ne peuvent retranscrire de nombreux cas rencontrés en industrie. Pour pouvoir analyser ces cas, il est nécessaire de les adapter `a l’analyse. Le deuxième constat porte sur l’adaptation qui n’est toujours pas simple surtout quand il existe une disparité sémantique entre les langages de description d’architecture et les modèles d’analyse ce qui nécessite de les rapprocher. Le dernier constat porte sur les difficultés dans la modélisation des systèmes distribués complexes car à moins de connaître le système complet, la représentation globale et sa validation temporelle reste coûteuse.Cette thèse propose des outils et méthodes pour améliorer le processus de modélisation et d’analyses temps réel. La première contribution consiste en la mise en place d’un référentiel de transformation de modèles endogène pour effectuer une adaptation conservative des modèles industriels aux modèles d’analyses. Dans l’optique de réduire l’écart sémantique entre les langages de description et les modèles d’analyse, cette thèse propose également une modélisation incrémentale des réseaux temps réel en vue de leur validation temporelle car les langages existants les considèrent de fa¸con limitée. La troisième contribution de la thèse porte sur la réduction des artéfacts de modélisation par extraction et élagage de méta-modèles afin d’obtenir les éléments nécessaires par rapport au points de vue d’analyse souhait´es.Toutes ces contributions sont implémentées dans des frameworks intégrant les processus d’analyses temps réel tels Time4Sys et MoSaRT et utilisées, dans le cadre d’un projet collaboratif, par des partenaires industriels. / The timing validation of real-time systems is mandatory for critical applications such as aeronautics,aerospace or automotive systems. The aim is to guarantee tasks response time and messages transmission time on networks. As for the criticality of these complex systems, it is necessary to implement a design process that reduces the development time therefore the time-to-market while reducing design errors risks.This context makes model-driven engineering well adapted for the development of critical real-time systems.The contributions of this thesis rely on the following observations. First of all, despite the existence of various analysis models, they often cannot represent perfectly some industrial cases. To analyze these cases,an adaptation is required to make them analyzable with existing tests. However, the adaptation is not quite easy especially in case of a semantic gap between systems description languages and analysis models. Also,several difficulties have been noticed to design and analyze an entire distributed complex system in one-shot unless knowing well the full system.In this PhD thesis, tools and methods are proposed to ease and improve the modeling and analysis processes of real-time systems. The first thesis contribution consists of implementing a rule-based endogenous transformation repository dedicated to adapt conservatively industrial models to the analysis models. The second contribution is focused on real-time networks and is dedicated to reduce the semantic gap between description languages and analysis models by proposing artefacts allowing to design networks on an incremental way. Moreover, this thesis proposes to reduce modeling artifacts using extraction and meta-models pruning inorder to retrieve useful elements referring to chosen analysis viewpoints.All these contributions are implemented in modeling frameworks integrating real-time analyses processes such as Time4Sys and MoSaRT, and used in a collaborative project by industrial partners.

La programmation par contraintes est une technologie pour l'optimisation qui associe des langages de modélisation riches avec des moteurs de résolution efficaces. Elle combine des techniques de plusieurs domaines tels que l'intelligence artificielle, la programmation mathématique et la théorie des graphes. Un défi majeur dans ce domaine concerne la définition de langages de haut-niveau pour faciliter la phase de modélisation des problèmes. Un autre aspect important est de concevoir des architectures robustes pour transformer des modèles de haut-niveau et obtenir des modèles exécutables efficaces, tout en visant plusieurs moteurs de résolution. Répondre à ces deux préoccupations est très difficile, car de nombreux aspects doivent être pris en compte, comme par exemple, l'expressivité et le niveau d'abstraction du langage ainsi que les techniques utilisées pour traduire le modèle de haut-niveau dans chacun des langages de résolution. Dans cette thèse, nous proposons une nouvelle perspective pour faire face à ces défis. Nous introduisons une nouvelle architecture pour la programmation par contraintes dans laquelle le problème est défini comme un ensemble d'objets contraints dans un nouveau langage de modélisation haut-niveau. La transformation des modèles est réalisée à l'aide de l'ingénierie des modèles. Les éléments des langages sont alors considérés comme des concepts définis dans un modèle de modèles appelé métamodèle. Cette nouvelle architecture permet d'aborder les phases de modélisation et de transformation de modèles en raisonnant à un niveau d'abstraction supérieur et, par conséquent, de réduire la complexité inhérente à ces deux phases.

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal

No description available.

Les appareils modernes sont constitués de plusieurs sous-systèmes de différentes sortes qui communiquent et interagissent. L'hétérogénéité de ces sous-systèmes et leurs interactions complexes rendent très délicate leur développement. L'approche d'ingénierie dirigée par les modèles apporte une solution en permettant l'expression de nombreux modèles structurels et comportementaux de natures très diverses. Dans ce contexte, il est nécessaire de construire un modèle unique qui intègre ces différents modèles afin d'y appliquer des méthodes de validation et de vérification pour permettre aux ingénieurs système de comprendre et de valider un comportement global. Cependant, la coordination manuelle des différents modèles qui composent le système est une opération source d'erreurs et les approches automatiques proposent des patrons de coordination ad-hoc pour certaines paires de langages. Dans ces approches, le patron de coordination est souvent encapsulé dans un outil dont il est difficile d'extraire les liens avec le système global. Cette thèse propose le Behavioral Coordination Operator Language (BCOoL), un langage dédié à la spécification de patrons de coordination entre des langages à partir de la définition d'opérateurs de coordination. Ces opérateurs sont employés afin d'automatiser la coordination de modèles exprimés dans ces langages. BCOoL est implémenté comme une suite de plugins qui s'appuient sur l'Eclipse Modeling Framework et présente ainsi un environnement complet pour l'exécution et la vérification de différents modèles coordonnés. / Modern devices embed several subsystems with different characteristics that communicate and interact in many ways. This makes its development complex since a designer has to deal with the heterogeneity of each subsystem but also with the interaction between them. To tackle the development of complex systems, Model Driven Engineering promotes the use of various, possibly heterogeneous, structural and behavioral models. In this context, the coordination of behavioral models to produce a single integrated model is necessary to provide support for validation and verification. It allows system designers to understand and validate the global and emerging behavior of the system. However, the manual coordination of models is tedious and error-prone, and current approaches to automate the coordination are bound to a fixed set of coordination patterns. Moreover, they encode the pattern into a tool thus limiting reasoning on the global system behavior. In this thesis, we propose a Behavioral Coordination Operator Language (B-COoL) to reify coordination patterns between specific domains by using coordination operators between the Domain-Specific Modeling Languages used in these domains. Those operators are then used to automate the coordination of models conforming to these languages. B-COoL is implemented as plugins for the Eclipse Modeling Framework thus providing a complete environment to execute and verify coordinated models. We illustrate the use of B-COoL with the definition of coordination operators between timed finite state machines and activity diagrams. We then use these operators to coordinate and execute the heterogeneous models of a surveillance camera system.

Cette thèse se situe à l'intersection de deux domaines-clés : l'ingénierie dirigée par les modèles (IDM) et les méthodes formelles, avec différents champs d'application. Elle porte sur la vérification formelle d'applications parallèles modélisées selon l'approche IDM. Dans cette approche, les modèles tiennent un rôle central et permettent de développer une application par transformations successives (automatisées ou non) entre modèles intermédiaires à différents niveaux d'abstraction, jusqu'à la production de code exécutable. Lorsque les modèles ont une sémantique formelle, il est possible d'effectuer une vérification automatisée ou semi-automatisée de l'application. Ces principes sont mis en oeuvre dans TOPCASED, un environnement de développement d'applications critiques embarquées basé sur ECLIPSE, qui permet la vérification formelle par connexion à des boîtes à outils existantes. Cette thèse met en oeuvre l'approche TOPCASED en s'appuyant sur la boîte à outils CADP pour la vérification et sur son plus récent formalisme d'entrée : LOTOS NT. Elle aborde la vérification formelle d'applications IDM à travers deux problèmes concrets : 1) Pour les systèmes GALS (Globalement Asynchrone Localement Synchrone), une méthode de vérification générique par transformation en LOTOS NT est proposée, puis illustrée sur une étude de cas industrielle fournie par AIRBUS : un protocole pour les communications entre un avion et le sol décrit dans le langage synchrone SAM conçu par AIRBUS. 2) Pour les services Web décrits à l'aide de la norme BPEL (Business Process Execution Language), une méthode de vérification est proposée, qui est basée sur une transformation en LOTOS NT des modèles BPEL, en prenant en compte les sous-langages XML Schema, XPath et WSDL sur lesquels repose la norme BPEL.

La programmation orientée langage (Language-Oriented Programming – LOP) préconise l’utilisation de langages de modélisation dédiés exécutables (eXecutable Domain-Specific Modeling Languages – xDSMLs) pour la conception, le développement, la vérification et la validation de systèmes hautement concurrents. De tels systèmes placent l’expression de la concurrence dans les langages informatiques au coeur du processus d’ingénierie logicielle, par exemple à l’aide de formalismes dédiés appelés modèles de concurrence (Models of Concurrency – MoCs). Ceux-ci permettent une analyse poussée du comportement des systèmes durant les phases de vérification et de validation, mais demeurent complexes à comprendre, utiliser, et maîtriser. Dans cette thèse, nous développons et étendons une approche qui vise à faire collaborer l’approche LOP et les MoCs à travers le développement de xDSMLs dans lesquels la concurrence est spécifiée de façon explicite (Concurrency-aware xDSMLs). Dans de tels langages, on spécifie l’utilisation systématique d’un MoC au niveau de la sémantique d’exécution du langage, facilitant l’expérience pour l’utilisateur final qui n’a alors pas besoin d’appréhender et de maîtriser l’utilisation du MoC choisi.Un tel langage peut être raffiné lors de la phase de déploiement, pour s’adapter à la plateforme utilisée, et les systèmes décrits peuvent être analysés sur la base du MoC utilisé. / Language-Oriented Programming (LOP) advocates designing eXecutable Domain-Specific Modeling Languages (xDSMLs) to facilitate the design, development, verification and validation of modern softwareintensive and highly-concurrent systems. These systems place their needs of rich concurrency constructs at the heart of modern software engineering processes. To ease theirdevelopment, theoretical computer science has studied the use of dedicated paradigms for the specification of concurrent systems, called Models of Concurrency (MoCs). They enable the use of concurrencyaware analyses such as detecting deadlocks or starvation situations, but are complex to understand and master. In this thesis, we develop and extend an approach that aims at reconciling LOP and MoCs by designing so-called Concurrencyaware xDSMLs. In these languages, the systematic use of a MoC is specified at the language level, removing from the end-user the burden of understanding or using MoCs. It also allows the refinement of the language for specific execution platforms, and enables the use of concurrency-aware analyses on the systems.

De nos jours, le degré de complexité des systèmes de transport notamment ferroviaires est important et grandissant. En effet, les nouvelles technologies et besoins des grandes métropoles contraignent les concepteurs de ces systèmes à toujours intégrer de plus en plus de fonctionnalités. Cette complexité rend obsolète les méthodes de conception traditionnelles qui reposent sur l'expertise d'ingénieurs. La conception du système est définie sur plusieurs documents de spécification, de centaines de pages chacun. Ces derniers comprennent généralement la description des différentes exigences, fonctionnalités et sous-systèmes, ils sont rédigés en langage naturel. Ceci est source d'erreurs et ambigüités lors des différentes phases de conception et de validation sécuritaire. De ce fait, l'ingénierie système basée sur les modèles propose des solutions outillées afin de structurer et spécifier de manière systématique le fonctionnement du système. Dans cette thèse, nous proposons une approche de rétro-ingénierie de ces spécifications système. Cette approche nous permet de définir une méthodologie orientée-scénarios pour la formalisation et analyse de spécifications système. Elle est basée sur le langage de modélisation semi-formel ScOLa (Scénarios Oriented Language) et un modèle d'exécution formel basé sur le langage AltaRica 3.0. Nous proposons, á partir de ScOLa, des techniques contribuant aux analyses de sûreté fonctionnelles du système. Ces techniques permettent de clarifier, structurer et analyser / As of today, the complexity of transportation systems and especially railways is continuously growing. Indeed, new technologies and needs of major metropolitan areas constrain system designers to integrate more and more functionalities. Traditional methods for the design of systems are mainly based on the knowledge of experts. Systems are specified in several documents, of hundreds of pages each. These documents provide a general description of the requirements, functionalities and sub-systems, and are written in a natural language. This is error-prone and source of ambiguities. Model-based systems engineering proposes systematic solutions to structure and specify systems architectures. In this thesis, we propose a reverse engineering approach that is able to capture systems concepts. This leads us to propose ScOLa, a scenario-oriented modeling language for systems specifications with the following features:- A scenario-oriented approach to provide a more contextual view of the system, at several abstraction levels.- A co-construction of the architecture and behavior of the system in the same model.- The use of ScOLa for a seamless integration of system specification and safety analysis. We propose ascenario-oriented methodology for safety analysis, implemented using AltaRica 3.0.

Cette thèse se situe à l'intersection de deux domaines-clés : l'ingénierie dirigée par les modèles (IDM) et les méthodes formelles, avec différents champs d'application. Elle porte sur la vérification formelle d'applications parallèles modélisées selon l'approche IDM. Dans cette approche, les modèles tiennent un rôle central et permettent de développer une application par transformations successives (automatisées ou non) entre modèles intermédiaires à différents niveaux d'abstraction, jusqu'à la production de code exécutable. Lorsque les modèles ont une sémantique formelle, il est possible d'effectuer une vérification automatisée ou semi-automatisée de l'application. Ces principes sont mis en oeuvre dans TOPCASED, un environnement de développement d'applications critiques embarquées basé sur ECLIPSE, qui permet la vérification formelle par connexion à des boîtes à outils existantes. Cette thèse met en oeuvre l'approche TOPCASED en s'appuyant sur la boîte à outils CADP pour la vérification et sur son plus récent formalisme d'entrée : LOTOS NT. Elle aborde la vérification formelle d'applications IDM à travers deux problèmes concrets : 1) Pour les systèmes GALS (Globalement Asynchrone Localement Synchrone), une méthode de vérification générique par transformation en LOTOS NT est proposée, puis illustrée sur une étude de cas industrielle fournie par AIRBUS : un protocole pour les communications entre un avion et le sol décrit dans le langage synchrone SAM conçu par AIRBUS. 2) Pour les services Web décrits à l'aide de la norme BPEL (Business Process Execution Language), une méthode de vérification est proposée, qui est basée sur une transformation en LOTOS NT des modèles BPEL, en prenant en compte les sous-langages XML Schema, XPath et WSDL sur lesquels repose la norme BPEL. / The work in this thesis is at the intersection of two major research domains~: Model-Driven Engineering (MDE) and formal methods, and has various fields of application. This thesis deals with the formal verification of parallel applications modelled by the MDE approach. In this approach, models play a central role and enable to develop an application through successive transformations (automated or not) between intermediate models of differing levels of abstraction, until executable code is produced. When models have a formal semantics, the application can be verified, either automatically or semi-automatically. These principles are used in TOPCASED, an ECLIPSE-based development environment for critical embedded applications, which enables formal verification by interconnecting existing tools. This thesis implements the TOPCASED approach by relying on the CADP toolbox for verifying systems, and on its most recent input formalism : LOTOS NT. This thesis tackles the formal verification of MDE applications through two real problems : 1) For GALS (Globally Asynchronous, Locally Synchronous), a generic verification method, based on a transformation to LOTOS NT, is proposed and illustrated by an industrial case-study provided by AIRBUS : a communication protocol between the airplane and the ground described in the synchronous langage SAM designed at AIRBUS. 2) For Web services specified with the BPEL (Business Process Execution Language) norm, a verification method is proposed. It is based on a BPEL to LOTOS NT transformation which takes into account XML Schema, Xpath, and WSDL, the languages on which the BPEL norm is built.

Depuis "toujours", en Génie Logiciel comme dans toutes les ingénieries, afin réduire la complexité et pour améliorer la réutilisation, le produit à construire est divisé en parties construites indépendamment et ensuite assemblées. L'approche récente de l'Ingénierie Dirigée par les Modèles (IDM, ou MDE pour Model-Driven Engineering), fait de même, en proposant "simplement" que les parties à construire et à assembler soient des modèles et non pas des programmes. C'est ainsi que le problème de la composition de modèles est devenu un thème important de l'IDM, et le sujet de cette thèse. En effet, un système logiciel réel est bien trop complexe pour pouvoir être décrit par un seul modèle. De nombreux modèles devront être créés pour le spécifier, soit à divers niveaux d'abstraction, soit selon divers points de vue, soit encore selon des domaines fonctionnels differents et complémentaires. Dans ce travail, nous partons de l'hypothèse que de tels domaines métiers existent. Un domaine est un champ d'expertise avec 1) les savoir-faire et les connaissances capturés et formalisés sous la forme d'un langage de modélisation dédié au domaine (un Domain-Specific Modeling Language (DSML)), et 2) des outils et des environnements supportant le développement d'applications dans ce domaine. Une application, dans un domaine, est décrite par un modèle (conforme au métamodèle du domaine). Dans ce travail, nous faisons aussi l'hypothèse que ces domaines sont exécutables ; les modèles du domaine sont exécutés par une machine virtuelle du domaine. En IDM, comme dans les autres approches du Génie Logiciel, la réutilisation impose que le processus d'assemblage des parties puisse se faire sans avoir à modifier celles-ci, ni bien sur l'environnement qui les a produit ou qui les exécute. Appliqué à notre contexte, cela signifie qu'il faut être capable de composer des modèles sans les modifier et sans modifier ni l'éditeur ni la machine virtuelle du domaine dont ils sont issus. C'est le problème que nous abordons dans notre travail. Nous montrons que pour atteindre cet objectif, il faut d'abord composer les domaines c'est à dire composer leurs métamodèles et leurs machines virtuelles, puis les modèles. Nous montrons dans ce travail comment ces compositions peuvent être réalisées sans modifier les éléments compos és, en utilisant des relations dites horizontales entre les métamodèles, et des liens entre les modèles. Cette approche est validée d'abord par la réalisation d'un certain nombre de domaines composites, et par de nombreuses compositions de modèles opérationnelles. Une partie importante du travail a consisté à définir Codèle, un langage de composition de modèles et de métamodèles, et à réaliser l'environnement d'assistance correspondant. Codèle assiste les ingénieurs pour composer de façon systématique les domaines, et rend automatique ou semi-automatique la composition de tous modèles provenant de ces domaines. Nous présentons l'outil Codèle et nous évaluons son usage dans divers projets.