This thesis describes code generation using design patterns. It deals with questions of specification of design patterns and their usage in code generation. The main part of thesis follows describtions of design patterns, their categorization, usage purpose and main ways of design patterns definitions. It describes the most often used formal design patterns specifications, their possible usage in code generation and design of algorithm for searching similar structures of patterns in source code in detail.

No description available.

Online gaming is today a popular everyday activity among both young people and adults. This has led to several new design methods such as dark game design patterns which aim to manipulate the user to act in a certain way that may not necessarily be in their best interest, with features that can be destructive to the user.  The purpose of this study is therefore to examine the presence of dark patterns on two popular gaming platforms – a free to play mobile game and a slot game at a popular online casino – to then investigate what the implementation of these patterns means for the given context. This was considered important to study to identify if the implementation of dark patterns is used differently depending on the gaming platform’s target group, especially as several studies show that it is mainly children and teenagers who play mobile games that are free to play, while slot games are aimed towards adults. The conclusion of this study has shown that the amount of identified dark patterns primarily depends on the game’s construction rather than it’s target group, but also that dark game design patterns are implemented to encourages the user to actively play online games, which in the long run should make the user want to support the gaming companies monetarily.

This thesis explores the design and implementation of a simulation framework created for C2 training environments, focusing on simulating the movement of aircraft and other moving targets between waypoints. The core objective was to develop an extensible, reliable, and realistic simulation system that can adapt to simulate a variety of entities, each characterized by unique movement patterns defined by their type. The simulated input scenarios involve a collection of targets, where each target traverses through a defined set of waypoints according to their specified movement behavior at initialization. The research involved a evaluation of established theories and ideologies of both aircraft and computer simulation, leading to the creation of a framework that leverages Java for its scalability and performance. The framework was designed from the ground up to promote extensibility of various types of moving targets beyond of just that of aircraft, such as helicopters, boats, missiles, and surface vehicles.  The accuracy of the simulation was tested by comparing its output to real-world flight data, demonstrating its capability to mimic realistic aircraft movement within predefined training scenarios. Additionally, the system's extensibility is showcased by simulating two different categories of aircraft—a commercial airliner and a small fighter jet—and illustrating the differences in their generated trajectories. Another outcome is the framework's ability to support real-time simulation, crucial for training scenarios in a C2 context. The system integrates and utilizes concurrent design techniques and dependable design patterns to ensure high throughput and performance, even when scaling to large numbers of targets. The framework's architecture allows for future extension and integration of new target types, without requiring modifications to the existing codebase, by the utilization of Javas SPI.

In den letzten Jahren haben Lernvideos im Bereich des informellen und formellen Lernens an Bedeutung gewonnen. Inwieweit Lernende bei der Nutzung von Videos unterstützt werden und Lehrende didaktische Szenarien umsetzen können, hängt jedoch von der eingesetzten Videolernumgebung ab. Es ist Anliegen der vorliegende Arbeit, Prinzipien des User Interface Designs sowie Komponenten und Mechanismen videobasierter Lehr-Lern-Szenarien in Bezug auf Videolernumgebungen zu identifizieren, zu beschreiben und technisch zu realisieren. Das Ziel besteht darin, Gestaltungsprinzipien in Form von Interaction Design Patterns zu erarbeiten und computergestützte videobasierte Lehr-Lern-Szenarien mit Hilfe von CSCL-Scripts durch eine geeignete Spezifikation und Formalisierung zu realisieren. Für die Erarbeitung der Interaction Design Patterns wurden 121 Videolernumgebungen hinsichtlich 50 Kategorien in einer Inhaltsanalyse empirisch untersucht und dokumentiert. Unter Berücksichtigung ähnlicher Patterns aus thematisch verwandten Pattern Languages und den Erfahrungen aus der Implementierung und dem Einsatz von Videolernumgebungen entstanden 45 Interaction Design Patterns für verbreitete Lösungen für wiederkehrende Probleme bei der Gestaltung und Entwicklung von Videolernumgebungen. Diese Patterns wurden auf Pattern Konferenzen diskutiert und im Anschluss evaluiert sowie bei der Konzeption, Entwicklung und Bewertung mehrerer Videolernumgebungen angewendet. Zudem wurde das Software Framework VI-TWO vorgestellt, mit dem sich fast alle Patterns auf einfache Weise in Web-Anwendungen realisieren lassen. Zur Spezifikation videobasierter CSCL-Scripts wurden existierende videobasierte und nicht videobasierte Scripts analysiert. Im Ergebnis unterschieden sich videobasierte CSCL-Scripts von allgemeinen CSCL-Scripts vor allem hinsichtlich der mit dem Video verknüpften oder darin verankerten Aufgaben und Aktivitäten. Videos werden dabei nicht als monolithische Einheiten, sondern als zeitkontinuierliche Medien betrachtet, in denen weitere Informationen zeitgenau verankert und Lernaktivitäten stattfinden können. Außerdem ließen sich drei Typen videobasierter CSCL-Scripts identifizieren: (1) Scripts zur Analyse und Diskussion von Videoinhalten, (2) Peer Annotation Scripts einschließlich dem Peer Assessment und (3) Jigsaw-Scripts, die das problembasierte Lernen mit Hilfe von Videos ermöglichen. Unabhängig davon variiert die Komplexität der Scripts auf drei Stufen: (1) sofern voneinander abgegrenzte zeitliche Phasen von Lernaktivitäten bestehen, (2) wenn darüber hinaus die Teilnehmer innerhalb von Gruppen Aufgaben bearbeiten (intra-group) und (3) falls außerdem Aufgaben auch gruppenübergreifend bearbeitet werden (inter-group). Auf Grundlage der Spezifikation konnte ein Datenmodell und ein Modell für die nutzerseitige Modellierung von Scripts verschiedener Komplexitätsstufen sowie Typen entwickelt und in dem CSCL-System VI-LAB realisiert werden. Diese Arbeit leistet in zweifacher Hinsicht einen Beitrag zur Forschung im Bereich E-Learning. Zum einen beschreiben die Interaction Design Patterns wiederkehrende User Interface Lösungen und stellen somit ein Hilfsmittel für Designer, Software Entwickler und Lehrende bei der Gestaltung und Implementierung von Videolernumgebungen dar. Zum anderen wurden durch die Spezifikation und softwareseitige Umsetzung videobasierter CSCL-Scripts Voraussetzungen geschaffen, die den praktischen Einsatz und die weitere Untersuchung des kollaborativen Lernens mit Videos ermöglichen.

In den letzten Jahren haben Lernvideos im Bereich des informellen und formellen Lernens an Bedeutung gewonnen. Inwieweit Lernende bei der Nutzung von Videos unterstützt werden und Lehrende didaktische Szenarien umsetzen können, hängt jedoch von der eingesetzten Videolernumgebung ab. Es ist Anliegen der vorliegende Arbeit, Prinzipien des User Interface Designs sowie Komponenten und Mechanismen videobasierter Lehr-Lern-Szenarien in Bezug auf Videolernumgebungen zu identifizieren, zu beschreiben und technisch zu realisieren. Das Ziel besteht darin, Gestaltungsprinzipien in Form von Interaction Design Patterns zu erarbeiten und computergestützte videobasierte Lehr-Lern-Szenarien mit Hilfe von CSCL-Scripts durch eine geeignete Spezifikation und Formalisierung zu realisieren. Für die Erarbeitung der Interaction Design Patterns wurden 121 Videolernumgebungen hinsichtlich 50 Kategorien in einer Inhaltsanalyse empirisch untersucht und dokumentiert. Unter Berücksichtigung ähnlicher Patterns aus thematisch verwandten Pattern Languages und den Erfahrungen aus der Implementierung und dem Einsatz von Videolernumgebungen entstanden 45 Interaction Design Patterns für verbreitete Lösungen für wiederkehrende Probleme bei der Gestaltung und Entwicklung von Videolernumgebungen. Diese Patterns wurden auf Pattern Konferenzen diskutiert und im Anschluss evaluiert sowie bei der Konzeption, Entwicklung und Bewertung mehrerer Videolernumgebungen angewendet. Zudem wurde das Software Framework VI-TWO vorgestellt, mit dem sich fast alle Patterns auf einfache Weise in Web-Anwendungen realisieren lassen. Zur Spezifikation videobasierter CSCL-Scripts wurden existierende videobasierte und nicht videobasierte Scripts analysiert. Im Ergebnis unterschieden sich videobasierte CSCL-Scripts von allgemeinen CSCL-Scripts vor allem hinsichtlich der mit dem Video verknüpften oder darin verankerten Aufgaben und Aktivitäten. Videos werden dabei nicht als monolithische Einheiten, sondern als zeitkontinuierliche Medien betrachtet, in denen weitere Informationen zeitgenau verankert und Lernaktivitäten stattfinden können. Außerdem ließen sich drei Typen videobasierter CSCL-Scripts identifizieren: (1) Scripts zur Analyse und Diskussion von Videoinhalten, (2) Peer Annotation Scripts einschließlich dem Peer Assessment und (3) Jigsaw-Scripts, die das problembasierte Lernen mit Hilfe von Videos ermöglichen. Unabhängig davon variiert die Komplexität der Scripts auf drei Stufen: (1) sofern voneinander abgegrenzte zeitliche Phasen von Lernaktivitäten bestehen, (2) wenn darüber hinaus die Teilnehmer innerhalb von Gruppen Aufgaben bearbeiten (intra-group) und (3) falls außerdem Aufgaben auch gruppenübergreifend bearbeitet werden (inter-group). Auf Grundlage der Spezifikation konnte ein Datenmodell und ein Modell für die nutzerseitige Modellierung von Scripts verschiedener Komplexitätsstufen sowie Typen entwickelt und in dem CSCL-System VI-LAB realisiert werden. Diese Arbeit leistet in zweifacher Hinsicht einen Beitrag zur Forschung im Bereich E-Learning. Zum einen beschreiben die Interaction Design Patterns wiederkehrende User Interface Lösungen und stellen somit ein Hilfsmittel für Designer, Software Entwickler und Lehrende bei der Gestaltung und Implementierung von Videolernumgebungen dar. Zum anderen wurden durch die Spezifikation und softwareseitige Umsetzung videobasierter CSCL-Scripts Voraussetzungen geschaffen, die den praktischen Einsatz und die weitere Untersuchung des kollaborativen Lernens mit Videos ermöglichen.:1 Einführung 19 1.1 Motivation 19 1.2 Herausforderungen und Forschungsfragen 20 1.2.1 Interaction Design Patterns 20 1.2.2 Videobasierte CSCL-Scripts 22 1.3 Kapitelübersicht und Forschungsmethoden 25 1.3.1 Kapitelübersicht 25 1.3.2 Forschungsmethoden je Kapitel 27 2 Lernen mit Videos 29 2.1 Terminologie, Einsatzfelder und Potentiale von Lernvideos 30 2.1.1 Begriffsbestimmung 30 2.1.2 Einsatzfelder und Szenarien für das Lernen mit Videos 32 2.1.3 Potentiale des Medium Video 34 2.2 Videos im Kontext kognitiver Lerntheorien 36 2.2.1 Theorie der kognitiven Last 36 2.2.2 Kognitive Theorie des Lernens mit Multimedia 38 2.3 Interaktivität audiovisueller Lernmedien 44 2.4 Lernformen 48 2.4.1 Rezeptives Lernen 49 2.4.2 Selbstgesteuertes Lernen 50 2.4.3 Kollaboratives Lernen 52 2.5 Zusammenfassung 56 3 Videolernumgebungen und Hypervideos 59 3.1 Terminologie und Modelle 60 3.1.1 Videolernumgebung 60 3.1.2 Terminologie: Video, Hypervideo und interaktives Video 62 3.1.3 Spezifikationen für Hypervideo-Dokumente 65 3.1.4 Modelle des zeitlichen Layouts 66 3.2 Human Video Interface 69 3.2.1 Gestaltungsraum von Hypervideos 70 3.2.2 Usability-Herausforderungen von Human Video Interfaces 74 3.3 Technische Herausforderungen 76 3.3.1 Download und Cache-Management / Echte Nicht-Linearität 77 3.3.2 Synchronisierung von Video und Annotationen 78 3.3.3 Adressierung und Abruf von Medienfragmenten 78 3.3.4 Deklarative Ansätze der Repräsentation von Multimedia 80 3.4 Produktion und Integration in Lernumgebungen 81 3.4.1 Produktion: Vorgehensweisen und Paradigmen 82 3.4.2 Integration in Lernumgebungen und Zusammenspiel mit Diensten im WWW 85 3.5 Zusammenfassung 87 4 Interaction Design Patterns für Videolernumgebungen 91 4.1 Einführung in Design Patterns 92 4.1.1 Design Patterns 95 4.1.2 Mustersprache 101 4.1.3 Verwandte Ansätze im Interaction Design 104 4.1.4 Verwandte Pattern Languages 106 4.2 Systematische Elaboration von Design Patterns 109 4.2.1 Stand der Forschung bzgldem Pattern Mining 110 4.2.2 Inhaltsanalyse von Videolernumgebungen 112 4.2.3 Analyse und Integration ähnlicher Muster bzwMustersprachen 128 4.2.4 Verfassen sowie Revision und Evaluation der Muster 130 4.2.5 Konstruktion der Pattern Language 135 4.3 Pattern Language für Videolernumgebungen 140 4.3.1 Struktur der Pattern Language 140 4.3.2 Angrenzende Mustersprachen 144 4.3.3 Repräsentation in einer Wissensbasis 145 4.3.4 Anwendungs- und Einsatzszenarien 148 4.3.5 Exemplarische Interaction Design Patterns 151 4.4 Zusammenfassung 168 5 Videobasierte CSCL-Scripts 171 5.1 Einführung 172 5.1.1 Hintergrund zu Scripts und CSCL-Scripts 172 5.1.2 Definition videobasierter CSCL-Scripts 175 5.1.3 Mehrwert und Potentiale 177 5.1.4 Typisierung videobasierter CSCL-Scripts 178 5.2 Spezifikation videobasierter CSCL-Scripts 184 5.2.1 Script-Komponenten 185 5.2.2 Script-Mechanismen 194 5.3 Modellierung von CSCL-Scripts 197 5.3.1 Komplexitätslevel 200 5.3.2 Verwandte Systeme und Ansätze zur Modellierung von Scripts 201 5.3.3 Konzept für eine formale Repräsentation 206 5.3.4 Konzept zur Modellierung im User Interface 209 5.4 Zusammenfassung 212 6 Realisierung von Patterns und Scripts 215 6.1 VI-TWO: JavaScript Framework für interaktive Videos 216 6.1.1 Anforderungen 217 6.1.2 Verwandte Arbeiten 219 6.1.3 Architektur von VI-TWO 222 6.1.4 Videoplayer 224 6.1.5 Videoannotationen 225 6.1.6 Makrointeraktivität in Kollektionen von Videos 229 6.1.7 Autorenwerkzeuge 232 6.2 VI-LAB: CSCL-System für videobasierte CSCL-Scripts 235 6.2.1 Anforderungen 236 6.2.2 Architektur von VI-LAB 238 6.2.3 Modellierung videobasierter CSCL-Scripts 241 6.2.4 Monitoring 244 6.3 Anwendungsbeispiele für VI-TWO und VI-LAB 246 6.3.1 Vi-Wiki 246 6.3.2 IWRM education 247 6.3.3 VI-LAB (Version 1) auf Basis von Wordpress 247 6.3.4 VI-LAB (Version 2) auf Basis von node.js 248 6.3.5 Theresienstadt explained 249 6.4 Zusammenfassung 252 7 Schlussbetrachtung 255 7.1 Beitrag der Arbeit zur Forschung 255 7.2 Kritische Würdigung 256 7.3 Ausblick 257

In this thesis, an improved framework is proposed for categorizing existing gamified systems. Related works and real world examples of gamification are discussed and some areas where insufficient research exists. In order to address the identified research problems, an experimental gamified system was designed and implemented for sharing articles related to different aspects of life. The participants of the study were recruited among the users of an existing Iranian lifestyle site for female users. Therefore, the gender of the users was considered in the design. A wide range of gamification elements were implemented in the system to test the effectiveness of specific design features and gamification elements’ parameters in increasing user motivation, for example, the contingency of rewards and the use of sound and animation in badges. A detailed questionnaire was used to answer the research questions. The results suggest specific combinations of gamification elements and their parameters that can be successfully applied by designers of social sites for similar audience.

La recherche en génie logiciel a depuis longtemps tenté de mieux comprendre le processus de développement logiciel, minimalement, pour en reproduire les bonnes pratiques, et idéalement, pour pouvoir le mécaniser. On peut identifier deux approches majeures pour caractériser le processus. La première approche, dite transformationnelle, perçoit le processus comme une séquence de transformations préservant certaines propriétés des données à l’entrée. Cette idée a été récemment reprise par l’architecture dirigée par les modèles de l’OMG. La deuxième approche consiste à répertorier et à codifier des solutions éprouvées à des problèmes récurrents. Les recherches sur les styles architecturaux, les patrons de conception, ou les cadres d’applications s’inscrivent dans cette approche. Notre travail de recherche reconnaît la complémentarité des deux approches, notamment pour l’étape de conception: dans le cadre du développement dirigé par les modèles, nous percevons l’étape de conception comme l’application de patrons de solutions aux modèles reçus en entrée. Il est coutume de définir l’étape de conception en termes de conception architecturale, et conception détaillée. La conception architecturale se préoccupe d’organiser un logiciel en composants répondant à un ensemble d’exigences non-fonctionnelles, alors que la conception détaillée se préoccupe, en quelque sorte, du contenu de ces composants. La conception architecturale s’appuie sur des styles architecturaux qui sont des principes d’organisation permettant d’optimiser certaines qualités, alors que la conception détaillée s’appuie sur des patrons de conception pour attribuer les responsabilités aux classes. Les styles architecturaux et les patrons de conception sont des artefacts qui codifient des solutions éprouvées à des problèmes récurrents de conception. Alors que ces artefacts sont bien documentés, la décision de les appliquer reste essentiellement manuelle. De plus, les outils proposés n’offrent pas un support adéquat pour les appliquer à des modèles existants. Dans cette thèse, nous nous attaquons à la conception détaillée, et plus particulièrement, à la transformation de modèles par application de patrons de conception, en partie parce que les patrons de conception sont moins complexes, et en partie parce que l’implémentation des styles architecturaux passe souvent par les patrons de conception. Ainsi, nous proposons une approche pour représenter et appliquer les patrons de conception. Notre approche se base sur la représentation explicite des problèmes résolus par ces patrons. En effet, la représentation explicite du problème résolu par un patron permet : (1) de mieux comprendre le patron, (2) de reconnaître l’opportunité d’appliquer le patron en détectant une instance de la représentation du problème dans les modèles du système considéré, et (3) d’automatiser l’application du patron en la représentant, de façon déclarative, par une transformation d’une instance du problème en une instance de la solution. Pour vérifier et valider notre approche, nous l’avons utilisée pour représenter et appliquer différents patrons de conception et nous avons effectué des tests pratiques sur des modèles générés à partir de logiciels libres. / Software engineering researchers have long tried to understand the software process development to mechanize it or at least to codify its good practices. We identify two major approaches to characterize the process. The first approach—known as transformational—sees the process as a sequence of property-preserving transformations. This idea was recently adopted by the OMG’s model-driven architecture (MDA). The second approach consists in identifying and codifying proven solutions to recurring problems. Research on architectural styles, frameworks and design patterns are part of this approach. Our research recognizes the complementarity of these two approaches, in particular in the design step. Indeed within the model-driven development context, we view software design as the process of applying codified solution patterns to input models. Software design is typically defined in terms of architectural design and detailed design. Architectural design aims at organizing the software in modules or components that meet a set of non-functional requirements while detailed design is—in some way—concerned by the contents of the identified components. Architectural design relies on architectural styles which are principles of organization to optimize certain quality requirements, whereas detailed design relies on design patterns to assign responsibilities to classes. Both architectural styles and design patterns are design artifacts that encode proven solutions to recurring design problems. While these design artifacts are documented, the decision to apply them remains essentially manual. Besides, once a decision has been made to use a design artifact, there is no adequate support to apply it to existing models. As design patterns present an ‘‘easier’’ problem to solve, and because architectural styles implementation relies on design patterns, our strategy for addressing these issues was to try to solve the problem for design patterns first, and then tackle architectural styles. Hence, in this thesis, we propose an approach for representing and applying design patterns. Our approach is based on an explicit representation of the problems solved by design patterns. Indeed, and explicit representation of the problem solved by a pattern enables to: 1) better understand the pattern, 2) recognize the opportunity of applying the pattern by matching the representation of the problem against the models of the considered system, and 3) specify declaratively the application of the pattern as a transformation of an instance of the problem into an instance of the solution. To verify and validate the proposed approach, we used it to represent and apply several design patterns. We also conducted practical tests on models generated from open source systems.

[pt] O desenvolvimento de software orientado a aspectos é um paradigma recente que introduz novas abstrações e mecanismos com o objetivo de melhorar a modularidade de interesses que se espalham pelo sistema. Entretanto, a satisfação de atributos de qualidade em sistemas orientados a aspectos não é tarefa simples e a utilização equivocada destas novas abstrações pode resultar em efeitos colaterais relacionados a princípios importantes da Engenharia de Software, tais como elevado acoplamento, baixa coesão dos módulos e incompleta modularidade dos interesses em aspectos. Problemas como estes não são facilmente verificáveis em sistemas de médio e grande porte sem um método adequado e, geralmente, consomem muito tempo e recursos. Portanto, torna-se necessário um método de avaliação que auxilie engenheiros de software na análise de sistemas orientados a aspectos. Este trabalho de mestrado propõe uma abordagem que provê suporte à avaliação quantitativa de implementações orientadas a aspectos. A abordagem incluiu: (i) um método de avaliação organizado em etapas, e (ii) uma ferramenta de medição e avaliação, chamada AJATO, que dá suporte ao método proposto. O método é composto por um conjunto de métricas e regras heurísticas. As métricas fornecem informações quantitativas e as heurísticas contribuem com algum raciocínio semântico dos números. A ferramenta AJATO é composta por quatro módulos que efetuam o parser do código, mapeamento de estruturas sintáticas em interesses, medição e avaliação heurística. Um conjunto de cinco estudos de caso envolvendo domínios de aplicação distintos foi realizado para avaliar a utilidade e usabilidade da abordagem proposta. / [en] Aspect-oriented software development is an emerging paradigm that provides new abstractions and mechanisms to support the modularization of crosscutting concerns through the software development lifecycle. However, the achievement of high-quality aspect-oriented software is not trivial. The inappropriate use of aspect-oriented abstractions and mechanisms potentially leads to the violation of important design principles, such as low coupling, high cohesion, incomplete modularization of crosscutting concerns into aspects, and so forth. These problems are not easily detectable and an ad hoc analysis of large designs and implementations is often expensive and time- consuming. Hence there is a need for an assessment method that assists software engineers in the analysis of their aspect-oriented implementations. This work proposes the development of a systematic approach to support the quantitative assessment of aspect-oriented software. The approach is organized in a stepwise fashion and is founded on a metrics suite and a comprehensive set of complementary rules. Our proposal is supported by a measurement and assessment tool. A set of five case studies from different application domains have been carried out in order to evaluate the usability and usefulness of our proposed approach.

Le travail de thèse présente une méthode de développement de systèmes automatisés basée sur les méthodes formelles B et TLA+. Le développement par raffinement est au cœur de la méthode proposée. Un système automatisé est modélisé par deux composants, un contrôlé formé par le dispositif physique et son environnement et un contrôleur pilotant ce dernier. Il est exprimé par un produit synchronisé sur les actions de ces deux composants. La première contribution de la thèse concerne la proposition d'une approche qui combine le B événementiel et le langage de modélisation TLA+ pour la vérification des propriétés de vivacité. Nous définissons une extension syntaxique et sémantique du B événementiel permettant d'exprimer des propriétés de vivacité. Nous développons un prototype pour la transformation d'un modèle B en un module TLA+ sur lequel nous effectuons la preuve des propriétés de vivacité avec le model checker TLC. Pour la vérification de ce type de propriétés sur des systèmes infinis, nous proposons l'utilisation des diagrammes de prédicats qui sont des abstractions des systèmes modélisés en TLA+. La deuxième contribution est la proposition d'une technique pour représenter explicitement le temps en B événementiel. Cette technique s'appuie sur la réalisation d'un entrelacement entre un processus qui gère le temps avec les autres processus du système. Le temps modélisé est discret et son écoulement est modélisé par des événements. Cette approche est assez différente des systèmes temporisés où l'on considère que le temps s'écoule indépendamment du système. Dans la troisième contribution, nous proposons une approche de développement des systèmes automatisés en utilisant la technique de composition où il s'agit de développer conjointement le contrôleur et le composant physique qu'il contrôle et appliquer le raffinement aussi bien sur le contrôleur que le contrôlé. Le raffinement est une technique de base des méthodes que nous proposons et si notre objectif est de construire des contrôleurs corrects, le critère de correction porte sur le comportement du système automatisé qui résulte de la composition du contrôleur et du contrôlé. Nous présentons également un théorème de compositionnalité qui indique sous quelles conditions il est possible de déduire que le composé des raffinements des contrôleur et contrôlé est un raffinement du composé des contrôleur et contrôlé abstraits. La dernière contribution porte sur la définition, la preuve et l'utilisation d'un patron de raffinement pour les processus continus dans des systèmes de production manufacturière. Ce type de patron prouvé permet d'utiliser l'abstraction discrète de l'effet d'un processus continu agissant pendant un certain temps / This thesis deals with the development of automated systems while following the formal methods B and TLA+. We propose a formal methodology based on the refinement paradigm to specify and verify the system that we model by two components: the controlled system representing the physical device and its environment, and the controller that controls the system. A synchronised product on the actions of these two components is applied to specify the automated system. As a first contribution, we propose an approach combining the event B method and the language TLA+ in order to verify liveness properties defined in user requirements. Inspired by the temporal logic of actions TLA, we first extend the event B notation to specify liveness properties and we give semantics of this extended syntax over traces. Second, we give transformation rules from a temporal B model into a TLA+ module. We present, in particular, our prototype system called B2TLA+, that we have developed to support this transformation. To consider infinite systems, we use predicate diagrams as abstractions of systems modelled with TLA+. To consider the real-time concept in automated systems, we propose as a second contribution a technique explicitly representing time in B event systems. This technique is based on an interleaving between any event handling time and the other system events. By considering the well known co-design technique, we propose as a third contribution a refinement-based composition technique keeping a separation between controller and controlled systems in order to build correct automated systems satisfying user requirements. We prove a compositionality theorem with respect to refinement to get an efficient approach to verify the refinement of a synchronized composition between components. We verify the refinement of a synchronized composition by verifying separately the refinement of each component. Finally, we define, prove and use in a case study as a fourth contribution the concept of a refinement pattern for continuous processes in manufacturing systems. Such proven pattern allows us to use the discrete abstraction of the effect of continuous processes operating for a while