Une idée centrale en ingénierie des systèmes est de construire les systèmes complexes par assemblage de composants. Chaque composant a ses propres caractéristiques, suivant différents points de vue, chacun mettant en évidence différentes dimensions d'un système. Un problème central est de définir le sens la composition de composants hétérogènes afin d'assurer leur interopérabilité correcte. Une source fondamentale d'hétérogénéité est la composition de sous-systèmes qui ont des différentes sémantiques d'execution et d' interaction. À un extrême du spectre sémantique on trouve des composants parfaitement synchronisés par une horloge globale, qui interagissent par transactions atomiques. À l'autre extrême, on a des composants complètement asynchrones, qui s'éxécutent à des vitesses indépendantes et interagissent nonatomiquement. Entre ces deux extrêmes, il existe une variété de modèles intermédiaires (par exemple, les modèles globalement asynchrones et localement synchrones). Dans ce travail, on étudie la combinaison des systèmes synchrones et asynchrones. A ce fin, on utilise BIP (Behavior-Interaction-Priority), un cadre général à base de composants permettant la conception rigoureuse de systémes. On définit une extension de BIP, appelée BIP synchrone, déstiné à modéliser les systèmes flot de données synchrones. Les pas d'éxécution sont décrites par des réseaux de Petri acycliquemunis de données et des priorités. Ces réseaux de Petri sont utilisés pour modéliser des flux concurrents de calcul. Les priorités permettent d'assurer la terminaison de chaque pas d'éxécution. Nous étudions une classe des systèmes synchrones ``well-triggered'' qui sont sans blocage par construction et le calcul de chaque pas est confluent. Dans cette classe, le comportement des composants est modélisé par des `graphes de flux modaux''. Ce sont des graphes acycliques représentant trois différents types de dépendances entre deux événements p et q: forte dépendance (p doit suivre q), dépendance faible (p peut suivre q) et dépendance conditionnelle (si p et q se produisent alors $p$ doit suivre q). On propose une transformation de modèles LUSTRE et MATLAB/Simulink discret à temps discret vers des systèmes synchrones ``well-triggered''. Ces transformations sont modulaires et explicitent les connexions entre composants sous forme de flux de données ainsi que leur synchronisation en utilisant des horloges. Cela permet d'intégrer des modèles synchrones dans les modèles BIP hétérogènes. On peut ensuite utiliser la validation et l'implantation automatique déjà disponible pour BIP. Ces deux traductions sont actuellement implementées et des résultats expérimentaux sont fournis. Pour les modèles BIP synchrones nous parvenons à générer du code efficace. Nous proposons deux méthodes: une implémentation séquentielle et une implémentation distribués. L'implémentation séquentielle consiste en une boucle infinie. L'implémentation distribuée transforme les graphes de flux modaux vers une classe particulieére de réseaux de Petri, que l'on peut transformer en réseaux de processus de Kahn. Enfin, on étudie la théorie de la conception de modeéles insensibles à la latence (latency-insensitive design, LID) qui traite le problème de latence des interconnexionsdans les systèmes synchrones. En utilisant la conception LID, les systèmes synchrones peuvent être «désynchronisés» en des réseaux de processus synchrones qui peuvent fonctionner à plus haute fréquence. Nous proposons un modèle permettant de construire des modéles insensibles à la latence en BIP synchrone, en représentant les mécanismes spécifiques d'interconnexion par des composants BIP synchrone. / A central idea in systems engineering is that complex systems are built by assembling com- ponents. Components have different characteristics, from a large variety of viewpoints, each highlighting different dimensions of a system. A central problem is the meaningful composition of heterogeneous components to ensure their correct interoperation. A fundamental source of heterogeneity is the composition of subsystems with different execution and interaction seman- tics. At one extreme of the semantic spectrum are fully synchronized components which proceed in a lockstep with a global clock and interact in atomic transactions. At the other extreme are completely asynchronous components, which proceed at independent speeds and interact non- atomically. Between the two extremes a variety of intermediate models can be defined (e.g. globally-asynchronous locally-synchronous models). In this work, we study the combination of synchronous and asynchronous systems. To achieve this, we rely on BIP (Behavior-Interaction-Priority), a general component-based framework encompassing rigorous design. We define an extension of BIP, called Synchronous BIP, dedicated to model synchronous data-flow systems. Steps are described by acyclic Petri nets equipped with data and priorities. Petri nets are used to model concurrent flow of computation. Priorities are instrumental for enforcing run-to-completion in the execution of a step. We study a class of well- triggered synchronous systems which are by construction deadlock-free and their computation within a step is confluent. For this class, the behavior of components is modeled by modal flow graphs. These are acyclic graphs representing three different types of dependency between two events p and q: strong dependency (p must follow q), weak dependency (p may follow q), conditional dependency (if both p and q occur then p must follow q). We propose translation of LUSTRE and discrete-time MATLAB/Simulink into well-triggered synchronous systems. The translations are modular and exhibit data-flow connections between components and their synchronization by using clocks. This allows for integration of synchronous models within heterogeneous BIP designs. Moreover, they enable the application of validation and automatic implementation techniques already available for BIP. Both translations are cur- rently implemented and experimental results are provided. For Synchronous BIP models we achieve efficient code generation. We provide two methods, sequential implementation and distributed implementation. The sequential implementation pro- duces endless single loop code. The distributed implementation transforms modal flow graphs to a particular class of Petri nets, that can be mapped to Kahn Process Networks. Finally, we study the theory of latency-insensitive design (LID) which deals with the problem of interconnection latencies within synchronous systems. Based on the LID design, synchronous systems can be “desynchronized” as networks of synchronous processes that might run with increased frequency. We propose a model for LID design in Synchronous BIP by representing specific LID interconnect mechanisms as synchronous BIP components.

L'importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d'application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s'intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d'outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l'influence du flot d'informations des entrées sur celui des sorties. Afin de répondre à la complexité croissante des systèmes temps-réels, nous étudions l'applicabilité de cette notion nouvelle au développement incrémental par raffinement et par composition. Le raffinement est abordé sous l'angle de la conservation de propriétés garantes de la correction du système au cours du processus de développement. Nous délimitons les conditions nécessaires et suffisantes à la conservation du délai de bout-en-bout lors d'un tel processus. De même, nous donnons des conditions suffisantes pour permettre le calcul du délai de bout-en-bout de manière compositionnelle. Combinés, ces résultats permettent d'établir un formalisme permettant la preuve du délai de bout-en-bout lors d'une démarche de développement incrémentale.

Une idée centrale en ingénierie des systèmes est de construire les systèmes complexes par assemblage de composants. Chaque composant a ses propres caractéristiques, suivant différents points de vue, chacun mettant en évidence différentes dimensions d'un système. Un problème central est de définir le sens la composition de composants hétérogènes afin d'assurer leur interopérabilité correcte. Une source fondamentale d'hétérogénéité est la composition de sous-systèmes qui ont des différentes sémantiques d'execution et d' interaction. À un extrême du spectre sémantique on trouve des composants parfaitement synchronisés par une horloge globale, qui interagissent par transactions atomiques. À l'autre extrême, on a des composants complètement asynchrones, qui s'éxécutent à des vitesses indépendantes et interagissent nonatomiquement. Entre ces deux extrêmes, il existe une variété de modèles intermédiaires (par exemple, les modèles globalement asynchrones et localement synchrones). Dans ce travail, on étudie la combinaison des systèmes synchrones et asynchrones. A ce fin, on utilise BIP (Behavior-Interaction-Priority), un cadre général à base de composants permettant la conception rigoureuse de systémes. On définit une extension de BIP, appelée BIP synchrone, déstiné à modéliser les systèmes flot de données synchrones. Les pas d'éxécution sont décrites par des réseaux de Petri acycliquemunis de données et des priorités. Ces réseaux de Petri sont utilisés pour modéliser des flux concurrents de calcul. Les priorités permettent d'assurer la terminaison de chaque pas d'éxécution. Nous étudions une classe des systèmes synchrones ''well-triggered'' qui sont sans blocage par construction et le calcul de chaque pas est confluent. Dans cette classe, le comportement des composants est modélisé par des 'graphes de flux modaux''. Ce sont des graphes acycliques représentant trois différents types de dépendances entre deux événements p et q: forte dépendance (p doit suivre q), dépendance faible (p peut suivre q) et dépendance conditionnelle (si p et q se produisent alors $p$ doit suivre q). On propose une transformation de modèles LUSTRE et MATLAB/Simulink discret à temps discret vers des systèmes synchrones ''well-triggered''. Ces transformations sont modulaires et explicitent les connexions entre composants sous forme de flux de données ainsi que leur synchronisation en utilisant des horloges. Cela permet d'intégrer des modèles synchrones dans les modèles BIP hétérogènes. On peut ensuite utiliser la validation et l'implantation automatique déjà disponible pour BIP. Ces deux traductions sont actuellement implementées et des résultats expérimentaux sont fournis. Pour les modèles BIP synchrones nous parvenons à générer du code efficace. Nous proposons deux méthodes: une implémentation séquentielle et une implémentation distribués. L'implémentation séquentielle consiste en une boucle infinie. L'implémentation distribuée transforme les graphes de flux modaux vers une classe particulieére de réseaux de Petri, que l'on peut transformer en réseaux de processus de Kahn. Enfin, on étudie la théorie de la conception de modeéles insensibles à la latence (latency-insensitive design, LID) qui traite le problème de latence des interconnexionsdans les systèmes synchrones. En utilisant la conception LID, les systèmes synchrones peuvent être "désynchronisés" en des réseaux de processus synchrones qui peuvent fonctionner à plus haute fréquence. Nous proposons un modèle permettant de construire des modéles insensibles à la latence en BIP synchrone, en représentant les mécanismes spécifiques d'interconnexion par des composants BIP synchrone.

L’importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d’application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s’intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d’outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l’influence du flot d’informations des entrées sur celui des sorties. Afin de répondre à la complexité croissante des systèmes temps-réels, nous étudions l’applicabilité de cette notion nouvelle au développement incrémental par raffinement et par composition. Le raffinement est abordé sous l’angle de la conservation de propriétés garantes de la correction du système au cours du processus de développement. Nous délimitons les conditions nécessaires et suffisantes à la conservation du délai de bout-en-bout lors d’un tel processus. De même, nous donnons des conditions suffisantes pour permettre le calcul du délai de bout-en-bout de manière compositionnelle. Combinés, ces résultats permettent d’établir un formalisme permettant la preuve du délai de bout-en-bout lors d’une démarche de développement incrémentale. / Real-time embedded systems are at the core of modern industrialized societies. They are a privileged target for the application of formal methods. The importance of real-time constraints in the specification of these systems requires the design of ad-hoc solutions. This work considers a class of real-time systems including those developed using OASIS, a tool-chain targeting hard real-time embedded systems developed at CEA LIST. We study the notion of end-to-end delay, which we propose to model as a constraint bearing directly on the influence of the input information flow over the output information flow . In order to cope with the growing complexity of real-time embedded systems, we study the possibility to apply this new notion of delay to the incremental development of such systems, by using both stepwise refinement and composition operators. We define the necessary and sufficient conditions to the preservation of the end-to-end delay by stepwise refinement. Similarly, we give sufficient conditions to compute the end-to-end delay in a compositional fashion. Together, these results permit to establish a formalism allowing to prove end-to-end delay properties in stepwise development methodologies.

Les systèmes intégrés sont aujourd’hui de plus en plus fréquemment confrontés à des contraintes de faible consommation ou d’efficacité énergétique. Ces problématiques se doivent d’être intégrées le plus en amont possible dans le flot de conception afin de réduire les temps de design et d’éviter de nombreuses itérations dans le flot. Dans ce contexte, le projet collaboratif HiCool, partenariat entre les laboratoires LIRMM et TIMA, les sociétés Defacto, Docea et ST Microelectronics, a mis en place une stratégie et un flot de conception pour concevoir des systèmes intégrés faible consommation tout en facilitant la réutilisation de blocks matériels (IPs) existants. L’approche proposée dans cette thèse s’intègre dans cette stratégie en apportant une petite dose d’asynchronisme dans des systèmes complètement synchrones. En effet, la réduction de la consommation est basée sur le constat que l’activation permanente de la totalité du circuit est inutile dans bien des cas. Néanmoins, contrôler l’activité avec des techniques de « clock gating » ou de « power gating » nécessitent usuellement d’effectuer un re-design du système et d’ajouter un organe de commande pour contrôler l’activation des zones effectuant un traitement. Le travail présenté dans ce manuscrit définit une stratégie basée sur des contrôleurs d’horloge et de domaine d’alimentation, asynchrones, distribués et facilement insérables dans un circuit avec un coût de re-design des plus réduit. / Today integrated systems are increasingly faced with the constraints of low consumption or energy efficiency. These issues need to be integrated as far upstream as possible in the design flow to reduce design time and avoid much iteration in the flow. In this context, the collaborative project HiCool, between LIRMM and TIMA laboratories, Defacto, Docea and ST Microelectronics companies, has set up a strategy and design flow to design integrated low power systems while facilitating the reuse of existing hardware blocks (IPs). The approach proposed in this thesis fits into this strategy by bringing a small dose of asynchrony in completely synchronous systems. Indeed, the reduction in consumption is based on the observation that permanent activation of the entire circuit is unnecessary in many cases. However, controlling the activity with techniques of "clock gating" or "power gating" usually need to perform a re-design of the system and to add a control device for controlling activation of areas effecting treatment. The work presented in this manuscript provides a strategy based clock controllers and power domain, asynchronous, distributed and easily insertable into a circuit with a low cost design.