Cette thèse s'intéresse à la modélisation et à l'analyse dessystèmes temps-réel distribués.Un système distribué est constitué de plusieurs composantsqui évoluent de manière partiellement indépendante. Lorsque des actionsexécutables par différentscomposants sont indépendantes, elles sont dites concurrentes.Dans ce cas, elles peuvent être exécutées dans n'importe quel ordre, sanss'influencer, et l'état atteint après ces actions ne dépend pas de leur ordred'exécution.Dans les systèmes temps-réel distribués, les contraintes de temps créent desdépendances complexes entre les composants et les événements qui ont lieu surces composants. Malgré l'omniprésence et l'aspect critique de ces systèmes,beaucoup de leurs propriétés restent encore à étudier.En particulier, la nature distribuée de ces systèmes est souvent laissée de côté.Notre travail s'appuie sur deux formalismesde modélisation: les réseaux de Petri temporels et les réseaux d'automatestemporisés, et est divisé en deux parties.Dans la première partie, nous mettons en évidence les différences entre lessystèmes temporisés centralisés et les systèmes temporisés distribués. Nouscomparons les formalismes principaux et leurs extensions, avec une approcheoriginale qui considère la concurrence.En particulier, nous montrons comment transformer un réseau de Petri temporelen un réseau d'automates temporisés qui a le même comportement distribué.Nous nous intéressons ensuite aux horloges partagées dans lesréseaux d'automates temporisés. Les horloges partagées sont problématiqueslorsque l'on envisage d'implanter ces modèles sur des architecturesdistribuées. Nous montrons comment se passer des horloges partagées, touten préservant le comportement distribué, lorsque cela est possible.Dans la seconde partie, nous nous attachons à formaliser les dépendancesentre les événements dans les représentations en ordre partieldes exécutions des réseaux de Petri (temporels ou non).Les réseaux d'occurrence sont une de ces représentations, et leur structuredonne directement les relations de causalité, conflit et concurrence entreles événements. Cependant, nous montrons que, même dans le cas non temporisé,certaines relations logiques entre les événements nepeuvent pas être directement décrites par ces relations structurelles.Après avoir formalisé les relations logiques en question, nous résolvons leproblème de synthèse suivant: étant donnée une formule logique qui décrit unensemble d'exécutions, construire un réseau d'occurrence associé,quand celui-ci existe.Nous étudions ensuite les relations logiques dans un cadre temporisé simplifié,et montrons que le temps crée des dépendances complexes entre les événements.Ces dépendances peuvent être utilisées pour définir des dépliages canoniques deréseaux de Petri temporels, dans ce cadre simplifié. / This thesis is concerned with the modeling and the analysis of distributedreal-time systems. In distributed systems, components evolve partlyindependently: concurrent actions may be performed in any order, withoutinfluencing each other and the state reached after these actions does notdepends on the order of execution. The time constraints in distributed real-timesystems create complex dependencies between the components and the events thatoccur. So far, distributed real-time systems have not been deeply studied, andin particular the distributed aspect of these systems is often left aside. Thisthesis explores distributed real-time systems. Our work on distributed real-timesystems is based on two formalisms: time Petri nets and networks of timedautomata, and is divided into two parts.In the first part, we highlight the differences between centralized anddistributed timed systems. We compare the main formalisms and their extensions,with a novel approach that focuses on the preservation of concurrency. Inparticular, we show how to translate a time Petri net into a network of timedautomata with the same distributed behavior. We then study a concurrency relatedproblem: shared clocks in networks of timed automata can be problematic when oneconsiders the implementation of a model on a multi-core architecture. We showhow to avoid shared clocks while preserving the distributed behavior, when thisis possible.In the second part, we focus on formalizing the dependencies between events inpartial order representations of the executions of Petri nets and time Petrinets. Occurrence nets is one of these partial order representations, and theirstructure directly provides the causality, conflict and concurrency relationsbetween events. However, we show that, even in the untimed case, some logicaldependencies between event occurrences are not directly described by thesestructural relations. After having formalized these logical dependencies, wesolve the following synthesis problem: from a formula that describes a set ofruns, we build an associated occurrence net. Then we study the logicalrelations in a simplified timed setting and show that time creates complexdependencies between event occurrences. These dependencies can be used to definea canonical unfolding, for this particular timed setting.

Ce manuscrit présente des travaux visant à intégrer un module d'ordonnancement (ProSched) à l'environnement de modélisation et simulation dynamique hybride PrODHyS dans le but d'automatiser la génération de scénarii de simulation de procédés discontinus sur la base d'une recette et d'une liste d'ordres de fabrication (OF). La méthodologie développée repose sur une approche mixte optimisation/simulation. Dans ce cadre, trois points essentiels ont été développés dans ces travaux : - tout d'abord, concevoir et développer des composants réutilisables (classes de recette) permettant de modéliser de manière hiérarchisée et systématique le déroulement des opérations unitaires. Pour cela, les notions de jeton Task et de macro-place paramétrable ont été introduites dans les RdPDO et permettent de décrire les recettes à réaliser par assemblage de ces composants prédéfinis. - ensuite, définir un modèle mathématique générique d'ordonnancement basé sur un formalisme de représentation bien établi (le R.T.N.) qui permet de modéliser les principales caractéristiques d'un procédé discontinu et de fournir l'ensemble des données d'entrée nécessaires au modèle de simulation. Pour cela, un modèle PLNE basé sur la formulation Unit Specific Event a été mis en œuvre. - enfin, définir l'interface existant entre le modèle d'optimisation et le modèle de simulation, à travers la notion de place de pilotage et de centre de décision au niveau du simulateur. Dans ce cadre, différentes stratégies de couplage sont proposées. Les potentialités de cette approche sont illustrées par la simulation d'un procédé complet. / This thesis presents works which aim to incorporate a scheduling module (ProSched) to an environment for modeling and dynamic hybrid simulation PrODHyS in order to automate the generation of scenarios for simulation of batch processes based on a recipe and a list of production orders (OF). The methodology developed is based on a mixed optimization / simulation approach. In this context, three key points have been developed in this work: - First, design and develop reusable components (recipe classes) for the hierarchical and systematic modeling of the sequencing of unit operations. For this, the notions of Task token and macro-place have been introduced in the RdPDO formalism and allow the modeling of recipes by assembling these predefined components. - Secondly, define a generic mathematical model of scheduling based on a well defined graphical formalism (RTN) that models the main characteristics of batch processes and provide all input data necessary to the simulation model. For this, a MILP model based on the Unit Specific Event formulation has been implemented. - Finally, define the interface between the optimization model and the simulation model through the concept of control place and decision-making center at the simulator level. In this context, various strategies of mixing optimization and simulation are proposed. The potential of this approach is illustrated by the simulation of a complete manufacturing process

Information flow properties are away of specifying security properties of systems ,dating back to the work of Goguen and Meseguer in the eighties. In this framework ,a system is modeled as having high-level (or confidential)events as well as low-level (or public) events, and a typical property requires that the high-level events should not “influence ”the occurrence of low-level events. In other words, the sequence of low-level events observed from a system execution should not reveal “too much” information about the high-level events that may have taken place. For example, the trace-based “non-inference” property states that for every trace produced by the system, its projection to low-level events must also be a possible trace of the system. For a system satisfying non-inference, a low-level adversary (who knows the language generated by the system) viewing only the low-level events in any execution cannot infer any in-formation about the occurrence of high-level events in that execution. Other well-known properties include separability, generalized non-interference, non-deducibility of outputs etc. These properties are trace-based. Similarly there is another class of properties based on the structure of the transition system called bisimulation-based information flow properties, defined by Focardiand Gorrieriin1995. In our thesis we study the problem of model-checking the well-known trace-based and bisimulation-based properties for some popular classes of infinite-state system models. We first consider trace-based properties. We define some language-theoretic operations that help to characterize language-inclusion in terms of satisfaction of these properties. This gives us a reduction of the language inclusion problem for a class of system models, say F, to the model-checking problem for F, whenever F, is effectively closed under these language-theoretic operations. We apply this result to show that the model-checking problem for Petri nets, push down systems and for some properties on deterministic push down systems is undecidable. We also consider the class of visibly pushdown systems and show that their model-checking problem is undecidable in general(for some properties).Then we show that for the restricted class of visibly pushdown systems in which all the high (confidential) event are internal, the model-checking problem becomes decidable. Similarly we show that the problem of model-checking bisimulation-based properties is undecidable for Petrinets, pushdown systems and process algebras. Next we consider the problem of detecting information leakage in programs. Here the programs are modeled to have low and high inputs and low outputs. The well known definition of“ non-interference” on programs says that in no execution should the low outputs depend on the high inputs. However this definition was shown to be too strong to be used in practice, with a simple(and considered to be safe)“password-checking” program failing it.“Abstract non-interference(ANI)”and its variants were proposed in the literature to generalize or weaken non-interference. We call these definitions qualitative refinements of non-interference. We study the problem of model-checking many classes of finite-data programs(variables taking values from a bounded domain)for these refinements. We give algorithms and show that this problem is in PSPACE for while, EXPTIME for recursive and EXPSPACE for asynchronous finite-data programs. We finally study different quantitative refinements of non-interference pro-posed in the literature. We first characterize these measures in terms of pre images. These characterizations potentially help designing analysis computing over and under approximations for these measures. Then we investigate the applicability of these measures on standard cryptographic functions.

Zum Verständnis menschlichen sozialen, administrativen und wirtschaftlichen Verhaltens, das als Spiel bzw. strategische Interaktion aufgefasst werden kann, reichen die rein analytischen Methoden nicht aus. Es ist nötig, Daten menschlichen strategischen Verhaltens zu sammeln. Basierend auf Daten lässt sich solches Verhalten modellieren, simulieren bzw. vorhersagen. Der theoretische Teil der Zielsetzung wird über praxisorientierte Konzeptualisierung strategischer Interaktion realer Agenten - Menschen und Maschinen - und gegenseitige Integration der Konzepte aus Spieltheorie und Multiagentensysteme erreicht, die über die bisherigen Ansätze hinausgehen. Der praktische Teil besteht darin, ein allgemein verwendbares System zu entwerfen, das strategische Interaktionen zwischen realen Agenten mit maximalen wissenschaftlichen Nutzen durchführen kann. Die tatsächliche Implementation ist eines der Ergebnisse der Arbeit. Ähnliche vorhandene Systeme sind GDL-Server (für Maschinen) [Genesereth u.a., 2005] und z-Tree (für Menschen) [Fischbacher, 2007]. Die Arbeit ist in drei Bereiche unterteilt - (1) Entwicklung von Sprachen für die Beschreibung eines Spiels, (2) ein auf diesen Sprachen basierendes Softwaresystem und (3) eine Offline-Analyse der u.a. mit dem System bereits gesammelten Daten als Beitrag zur Möglichkeiten der Verhaltensbeschreibung. Die Innovation dieser Arbeit besteht nicht nur darin ,einzelne Bereiche mit einander zu kombinieren, sondern auch Fortschritte auf jedem Bereich für sich allein zu erreichen. Im Bereich der Spielbeschreibungssprachen, werden zwei Sprachen - PNSI und SIDL - vorgeschlagen, die beide Spiele bei imperfekter Information in diskreter Zeit definieren können. Dies ist ein Fortschritt gegenüber der bisherigen Sprachen wie Gala und GDL. Speziell die auf Petrinetzen basierende Sprache PNSI kann gleichermaßen für Gameserver und für spieltheoretische Algorithmen von z.B. GAMBIT verwendet werden. Das entwickelte System FRAMASI basiert auf JADE [Bellifemine u.a., 2001] und ist den bisherigen Client-Server-Lösungen durch Vorteile der Multiagentensysteme voraus. Mit dem entstandenen System wurde bereits ein Experiment entsprechend den Standards der experimentellen Spieltheorie durchgeführt und somit die Praxistauglichkeit nachgewiesen. Das Experiment hatte als Ziel, Daten zur menschlichen Unvorhersagbarkeit und zur Vorhersagefähigkeit anderer zu liefen. Dafür wurden Varianten von \"Knobeln\" verwendet. Die Daten dieses Experiments sowie eines Experiments einer externen Arbeitsgruppe mit ähnlicher Motivation wurden mit Hilfe von Datamining analysiert. Dabei wurden die in der Literatur berichteten Gesetzmäßigkeiten des Verhaltens nachgewiesen und weitere Gesetzmäßigkeiten entdeckt.:Einführung Grundlagen Verwandte Arbeiten Sprachen für Spielbeschreibung Implementation der Spielinfrastruktur Beschreibung Strategischen Verhaltens Resümee Ergebnisse Ausblick / To understand human social, administrative and economic behavior, which can be considered as a game or strategic interaction, the purely analytical methods do not suffice. It is necessary to gather data of human strategic behavior. Based on data, one can model, simulate and predict such behavior. The theoretical part of the objective is achieved using a practice oriented conceptualization of the real agents\' - humans and machines - strategic interaction and mutual integration of the concepts from game theory and multi-agent systems, which go beyond the related work. The practical part is the design of an universally usable system that can perform the strategic interactions between real agents with maximum scientific benefit. The current implementation is one of the results of the work. Similar existing systems are GDL-server (for machines) [Genesereth et al., 2005] and z-Tree (for humans) [Fischbacher, 2007]. The work is divided in three fields - (1) development of languages for the description of a game, (2) a software system based on these languages and (3) an offline analysis of the data already gathered among other things using the system as a contribution to behavior definition facilities. The innovation of this work does not consist only in combining of the several fields to each other, but also in achieving of improvements in every field on its own. In the field of game definition languages, two languages are proposed - PNSI and SIDL, which both can define games of imperfect information in discrete time. It is an improvement comparing with hitherto languages as Gala and GDL. Especially, the Petri net based language PNSI can likewise be used for game servers and game theoretic algorithms like GAMBIT. The developed system FRAMASI is based on JADE [Bellifemine et al., 2001] and is ahead of the hitherto client-server solutions through the advantages of the multi-agent systems. Using the originated system, an experiment has been conducted according to the standards from the experimental game theory, and thus demonstrated the practicability. The experiment had the objective to provide data on the human unpredictability and the ability to predict others. Therefore, variants of Roshambo were used. The data from this experiment and from an experiment of an external workgroup with a similar motivation were analyzed using data mining. As results, the regularities of the behavior reported in literature have been demonstrated and further regularities have been discovered.:Einführung Grundlagen Verwandte Arbeiten Sprachen für Spielbeschreibung Implementation der Spielinfrastruktur Beschreibung Strategischen Verhaltens Resümee Ergebnisse Ausblick