No description available.

No description available.

This thesis presents two proactive resource allocation algorithms, RBA* and OBA, for asynchronous real-time distributed systems. The algorithms consider an application model where timeliness requirements are expressed using Jensen's benefit functions and propose adaptation functions to describe anticipated workload for future time intervals. Furthermore, an adaptation model is considered where processes are replicated for sharing workload increases. A real-time Ethernet system model is considered where message collisions are resolved. Given such models, the objective is to maximize aggregate application benefit and minimize aggregate missed deadline ratio. Since determining the optimal allocation is computationally intractable, the algorithms heuristically compute the allocation so that it is as "close" as possible to the optimal allocation. While RBA* analyzes process response times to determine the allocation, OBA analyzes processor overloads to compute the decision in a much faster way. RBA* incurs a quadratic amortized complexity in terms of subtask arrivals for the most computationally intensive component when DASA is used as the underlying process-scheduling algorithm, whereas OBA incurs a logarithmic amortized complexity for the corresponding component. To study how different process-scheduling and message-scheduling algorithms affect the performance of the algorithms and to compare their performances, benchmark-driven experiments were conducted. The experimental results reveal that RBA* produces higher aggregate benefit and lower missed deadline ratio when DASA is used for process scheduling and message scheduling. Furthermore, it is observed that RBA* produces higher aggregate benefit and lower missed deadline ratio than OBA, confirming the intuition that accurate response time analysis can lead to better results. / Master of Science

No description available.

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.

This thesis focuses on problem-solution analysis of synchronous digital circuits; the results of which are autosynchronous circuit design methodology, timing parameter definitions based on simulation models and constraint settings. The RTL transformation of the synchronous state machine in VHDL language to an autosynchronous state machine was created with minimal modifications for the simple design of these circuits. Following this, a comparison of the transformed state machines with their synchronous originals in parameters such as chip area, current consumption and timing specification domain is introduced. The summation of this thesis displays a theoretical comparison of several types of synchronization (synchronous, autosynchronous, fundamental asynchronous, EAIC, Bundled-data, Dual-rail) which are presented on the single state machine example with the same technology parameters.

No description available.