Nous avons étudié dans le cadre de cette thèse le design, la vérification et l'implémentation des systèmes à composants. Nous nous sommes intéressés en particulier aux formalismes exprimant des interactions complexes, dans lesquels les connecteurs servent non seulement au transfert de données mais également à la synchronisation entre composants. 1. DESIGN ET VÉRIFICATION Le design par contrat est une approche largement répandue pour développer des systèmes lorsque plusieurs équipes travaillent en parallèle. Les contrats représentent des contraintes sur les implémentations qui sont préservées tout au long du développement et du cycle de vie d'un système. Ils peuvent donc servir également à la phase de vérification d'un tel système. Notre but n'est pas de proposer un nouveau formalisme de spécification, mais plutôt de définir un ensemble minimal de propriétés qu'une théorie basée sur les contrats doit satisfaire pour permettre certains raisonnements. En cela, nous cherchons à séparer explicitement les propriétés spécifiques à chaque formalisme de spécification et les règles de preuves génériques. Nous nous sommes attachés à fournir des définitions suffisamment générales pour exprimer un large panel de langages de spécification, et plus particulièrement ceux dans lesquels les interactions sont complexes, tels que Reo ou BIP. Pour ces derniers, raisonner sur la structure du système est essentiel et c'est pour cette raison que nos contrats ont une partie structurelle. Nous montrons comment découle de la propriété nommée raisonnement circulaire une règle pour prouver la dominance sans composer les contrats, et comment cette propriété peut être affaiblie en utilisant plusieurs relations de raffinement. Notre travail a été motivé par les langages de composants HRC L0 et L1 définis dans le projet SPEEDS. 2. IMPLÉMENTATION Synthétiser un contrôleur distribué imposant une contrainte globale sur un système est dans le cas général un problème indécidable. On peut obtenir la décidabilité en réduisant la concurrence: nous proposons une méthode qui synchronise les processus de façon temporaire. Dans les travaux de Basu et al., le contrôle distribué est obtenu en pré-calculant par model checking la connaissance de chaque processus, qui reflète dans un état local donné toutes les configurations possibles des autres processus. Ensuite, à l'exécution, le contrôleur local d'un processus décide si une action peut être exécutée sans violer la contrainte globale. Nous utilisons de même des techniques de model checking pour pré-calculer un ensemble minimal de points de synchronisation au niveau desquels plusieurs processus partagent leur connaissance au court de brèves périodes de coordination. Après chaque synchronisation, les processus impliqués peuvent de nouveau progresser indépendamment les uns des autres jusqu'à ce qu'une autre synchronisation ait lieu. Une des motivations pour ce travail est l'implémentation distribuée de systèmes BIP. / In this thesis, we have studied how component-based systems are designed, verified and then implemented. We have focused in particular on formalisms involving complex interactions, where connectors are not only used to transfer data but also play a role in the synchronization of components. 1. DESIGN AND VERIFICATION Contracts are emerging as a concept of choice when systems are designed by teams working independently. They are design constraints for implementations which are maintained throughout the development and life cycle of the system, thus being also useful for verification. Our goal is not to propose a new design framework but rather to define a minimal set of properties which a given contract theory should satisfy to offer some reasoning rules. In that sense, we aim at a separation of concerns between framework-dependent properties and generic proof rules. We have focused on finding definitions expressive enough to encompass a great variety of existing specification formalisms, and in particular those in which interaction is complex, like Reo and BIP. For those, reasoning about the structure of the system is essential and this is why our contracts have a structural part. We show how so-called circular reasoning entails a rule for proving dominance (refinement between contracts) without composing contracts and how it can be relaxed by combining several refinement relations. Our work has a practical motivation in the component frameworks HRC L0 and L1 defined in the SPEEDS IP project. 2. IMPLEMENTATION The problem of synthesizing a distributed controller that imposes some global constraint on a system is, in general, undecidable. One can achieve decidability at the expense of reducing concurrency: we propose a method that synchronizes processes temporarily. In Basu et al., distributed control is achieved by first using model checking to precalculate the knowledge of each process, which reflects in a given local state all the possible situations of the other processes. Then, at runtime, the local controller of a process decides whether an action of that process can be executed without violating the imposed constraint. We use model checking techniques as well to precalculate a minimal set of synchronization points, where joint knowledge, i.e., knowledge common to several processes, can be achieved during short coordination phases. After each synchronization, the participating processes can again progress independently until a further synchronization is called for. One practical motivation for this work is the distributed implementation of BIP systems.

Thesis (Ph. D.)--Ohio State University, 2007. / Title from first page of PDF file. Includes bibliographical references (p. 204-214).

Cache memory is used, in most single-core and multi-core processors, to improve performance by bridging the speed gap between the main memory and CPU. Even though cache increases performance, it poses some serious challenges for embedded systems running real-time applications. Cache introduces execution time unpredictability due to its adaptive and dynamic nature and cache consumes vast amount of power to be operated. Energy requirement and execution time predictability are crucial for the success of real-time embedded systems. Various cache optimization schemes have been proposed to address the performance, power consumption, and predictability issues. However, currently available solutions are not adequate for real-time embedded systems as they do not address the performance, power consumption, and execution time predictability issues at the same time. Moreover, existing solutions are not suitable for dealing with multi-core architecture issues. In this dissertation, we develop a methodology through cache optimization for real-time embedded systems that can be used to analyze and improve execution time predictability and performance/power ratio at the same time. This methodology is effective for both single-core and multi-core systems. First, we develop a cache modeling and optimization technique for single-core systems to improve performance. Then, we develop a cache modeling and optimization technique for multi-core systems to improve performance/power ratio. We develop a cache locking scheme to improve execution time predictability for real-time systems. We introduce Miss Table (MT) based cache locking scheme with victim cache (VC) to improve predictability and performance/power ratio. MT holds information about memory blocks, which may cause more misses if not locked, to improve cache locking performance. / VC temporarily stores the victim blocks from level-1 cache to improve cache hits. In addition, MT is used to improve cache replacement performance and VC is used to improve cache hits by supporting stream buffering. We also develop strategies to generate realistic workload by characterizing applications to simulate cache optimization and cache locking schemes. Popular MPEG4, H.264/AVC, FFT, MI, and DFT applications are used to run the simulation programs. Simulation results show that newly introduced Miss Table based cache locking scheme with victim cache significantly improves the predictability and performance/power ratio. In this work, a reduction of 33% in mean delay per task and a reduction of 41% in total power consumption are achieved by using MT and VCs while locking 25% of level-2 cache size in an 4-core system. It is also observed that execution time predictability can be improved by avoiding more than 50% cache misses while locking one-fourth of the cache size. / by Abu Asaduzzaman. / Vita. / Thesis (Ph.D.)--Florida Atlantic University, 2009. / Includes bibliography. / Electronic reproduction. Boca Raton, Fla., 2009. Mode of access: World Wide Web.

Das Thema Information Retrieval hat insbesondere in Form von Internetsuchmaschinen eine große Bedeutung erlangt. Retrievalsysteme werden für eine Vielzahl unterschiedlicher Rechercheszenarien eingesetzt, unter anderem für firmeninterne Supportdatenbanken, aber auch für die Organisation persönlicher E-Mails. Eine aktuelle Herausforderung besteht in der Bestimmung und Vorhersage der Leistungsfähigkeit einzelner Komponenten dieser Retrievalsysteme, insbesondere der komplexen Wechselwirkungen zwischen ihnen. Für die Implementierung und Konfiguration der Retrievalsysteme und der Retrievalkomponenten werden Fachleute benötigt. Mithilfe der webbasierten Lernanwendung Xtrieval Web Lab können Studierende praktisches Wissen über den Information Retrieval Prozess erwerben, indem sie Retrievalkomponenten zu einem Retrievalsystem zusammenstellen und evaluieren, ohne dafür eine Programmiersprache einsetzen zu müssen. Spielemechaniken leiten die Studierenden bei ihrem Entdeckungsprozess an, motivieren sie und verhindern eine Informationsüberladung durch eine Aufteilung der Lerninhalte. / Information retrieval has achieved great significance in form of search engines for the Internet. Retrieval systems are used in a variety of research scenarios, including corporate support databases, but also for the organization of personal emails. A current challenge is to determine and predict the performance of individual components of these retrieval systems, in particular the complex interactions between them. For the implementation and configuration of retrieval systems and retrieval components professionals are needed. By using the web-based learning application Xtrieval Web Lab students can gain practical knowledge about the information retrieval process by arranging retrieval components in a retrieval system and their evaluation without using a programming language. Game mechanics guide the students in their discovery process, motivate them and prevent information overload by a partition of the learning content.