No description available.

Formal methods offer a way to deal with the complexity of information systems. They are adapted to a variety of domains like design, verification, model-checking, test and supervision. But information systems are also more and more often distributed, first because of the generalization of information networks, but also because inside a single device, like a computer, the numerous components run concurrently. The problem is that concurrency is known to be a major difficulty for the use of formal methods because it causes a combinatorial explosion of the state space of the systems. This difficulty comes sometimes with another one due to time when it plays an important role in the behaviour of the systems, for instance when the execution time is a critical parameter. These two difficulties, concurrency and real-time, have guided my research works. Sometimes I have tackled one of these two aspects separately, but in many of my works, I have dealt with the problems that arise when one studies systems that are both concurrent and real-time. In my habilitation thesis, I give an overview of my recent research works on dependencies between events in real-time distributed systems and on implementability issues for these systems.

No description available.

In this thesis, we present a MAC-layer packet scheduling algorithm, called Best-effort Packet Scheduling Algorithm(BPA), for real-time switched Ethernet networks. BPA considers a message model where application messages have trans-node timeliness requirements that are specified using Jensen's benefit functions. The algorithm seeks to maximize aggregate message benefit by allowing message packets to inherit benefit functions of their parent messages and scheduling packets to maximize aggregate packet-level benefit. Since the packet scheduling problem is NP-hard, BPA heuristically computes schedules with a worst-case cost of O(n^2), faster than the O(n^3) cost of the best known Chen and Muhlethaler's Algorithm(CMA) for the same problem. Our simulation studies show that BPA performs the same or significantly better than CMA. We also construct a real-time switched Ethernet by prototyping an Ethernet switch using a Personal Computer(PC) and implementing BPA in the network protocol stack of the Linux kernel for packet scheduling. Our actual performance measurements of BPA using the network implementation reveal the effectiveness of the algorithm. Finally, we derive timeliness feasibility conditions of real-time switched Ethernet systems that use the BPA algorithm. The feasibility conditions allow real-time distributed systems to be constructed using BPA, with guaranteed soft timeliness. / Master of Science

Cette thèse traite de systèmes embarqués contrôlés par un ensemble de processus périodiques non synchronisés. Chaque processus est activé quasi-périodiquement, c'est-à-dire périodiquement avec une gigue bornée. Les délais de communication sont également bornés. De tels systèmes réactifs, appelés 'quasi-périodiques', apparaissent dès que l'on branche ensemble deux processus périodiques. Dans la littérature, ils sont parfois qualifiés de systèmes distribués temps-réels synchrones. Nous nous intéressons aux techniques de conception et d'analyse de ces systèmes qui n'imposent pas de synchronisation globale. Les langages synchrones ont été introduits pour faciliter la conception des systèmes réactifs. Ils offrent un cadre privilégié pour programmer, analyser, et vérifier des systèmes quasi-périodiques. En s'appuyant sur une approche synchrone, les contributions de cette thèse s'organisent selon trois thématiques: vérification,implémentation, et simulation des systèmes quasi périodiques.Vérification: 'L'abstraction quasi-synchrone' est une abstraction discrète proposée par Paul Caspi pour vérifier des propriétés de sûreté des systèmes quasi-périodiques. Nous démontrons que cette abstraction est en général incorrecte et nous donnons des conditions nécessaires et suffisantes sur le graphe de communication et les caractéristiques temps-réel de l'architecture pour assurer sa correction. Ces résultats sont ensuite généralisés aux systèmes multi-périodiques.Implémentation: Les 'LTTAs' sont des protocoles conçus pour assurer l'exécution correcte d'une application sur un système quasi-périodique. Nous proposons d'étudier les LTTA dans un cadre synchrone unifié qui englobe l'application et les contrôleurs introduits par les protocoles. Cette approche nous permet de simplifier les protocoles existants, de proposer des versions optimisées, et de donner de nouvelles preuves de correction. Nous présentons également dans le même cadre un protocole fondé sur une synchronisation d'horloge pour comparer les performances des deux approches.Simulation: Un système quasi-périodique est un exemple de modèle faisant intervenir des caractéristiques temps-réels et des tolérances. Pour ce type de modèle non déterministe, nous proposons une 'simulation symbolique', inspirée des techniques de vérification des automates temporisés. Nous montrons comment compiler un modèle mêlant des composantes temps-réel non déterministes et des contrôleurs discrets en un programme discret qui manipule des ensembles de valeurs. Chaque trace du programme résultant capture un ensemble d'exécutions possibles du programme source. / In this thesis we study embedded controllers implemented as sets of unsynchronized periodic processes. Each process activates quasi-periodically, that is, periodically with bounded jitter, and communicates with bounded transmission delays. Such reactive systems,termed 'quasi-periodic', exist as soon as two periodic processes areconnected together. In the distributed systems literature they arealso known as synchronous real-time models. We focus on techniquesfor the design and analysis of such systems without imposing a globa lclock synchronization. Synchronous languages were introduced as domain specific languages for the design of reactive systems. They offer an ideal framework to program, analyze, and verify quasi-periodic systems. Based on a synchronous approach, this thesis makes contributions to the treatment of quasi-periodic systems along three themes: verification,implementation, and simulation.Verification: The 'quasi-synchronous abstraction' is a discrete abstraction proposed by Paul Caspi for model checking safety properties of quasi-periodic systems. We show that this abstractionis not sound in general and give necessary and sufficient conditionson both the static communication graph of the application and the real-time characteristics of the architecture to recover soundness. We then generalize these results to multirate systems.Implementation: 'Loosely time-triggered architectures' are protocols designed to ensure the correct execution of an application running on a quasi-periodic system. We propose a unified framework that encompasses both the application and the protocol controllers. This framework allows us to simplify existing protocols, propose optimized versions, and give new correctness proofs. We instantiate our framework with a protocol based on clock synchronization to compare the performance of the two approaches.Simulation: Quasi-periodic systems are but one example of timed systems involving real-time characteristics and tolerances. For such nondeterministic models, we propose a 'symbolic simulation' scheme inspired by model checking techniques for timed automata. We show how to compile a model mixing nondeterministic continuous-time and discrete-time dynamics into a discrete program manipulating sets of possible values. Each trace of the resulting program captures a set of possible executions of the source program.