De nos jours, les services Web sont très utilisés notamment par les entreprises pour rendre accessibles leurs métiers, leurs données et leurs savoir-faire via le Web. L'émergence des services Web a permis aux applications d'être présentées comme un ensemble de services métiers bien structurés et correctement décrits, plutôt que comme un ensemble d'objets et de méthodes. La composition automatique de services est une tâche complexe mais qui rend les services interopérables, ainsi leur interaction permet d'offrir une valeur ajoutée dans le traitement des requêtes des utilisateurs en prenant en compte des critères fonctionnels et non fonctionnels de la qualité de service. Dans ce travail de thèse, nous nous intéressons plus précisément aux services à base de localisation (LBS) qui permettent d'intégrer des informations géographiques, et de fournir des informations accessibles depuis des appareils mobiles via, les réseaux mobiles en faisant usage des positions géographiques de ces appareils. L'objectif de ce travail est de proposer une approche orientée modèles pour spécifier, valider et mettre en œuvre des processus de composition automatique de services à des fins de sécurité routière dans les transports. Cette approche est basée sur deux outils formels à savoir les Réseaux de Petri (RdP) et l'algèbre (max,+). Pour cela, nous préconisons l'utilisation des workflow patterns dans la composition, où chaque pattern est traduit par un modèle RdP et ensuite par une équation mathématique dans l'algèbre (max,+). Les modèles formels développés ont conduits, d'une part, à la description graphique et analytique des processus considérés, et d'autre part, à l'évaluation et la vérification quantitatives et qualitatives de ces processus. Une plateforme, appelée TransportML, pour la collaboration et l'interopérabilité de services à base de positionnement a été implémentée. Les résultats obtenus par la simulation des modèles formels sont comparés à ceux issus des simulations du fonctionnement de la plateforme et des expérimentations sur le terrain.Cette thèse est effectuée dans le cadre des projets Européens FP7 ASSET (2008-2011) et TeleFOT (2008-2012).

Le travail présenté s'inscrit dans le contexte de la théorie des systèmes linéaires dans les dioïdes. La motivation initiale de cette étude a été de contribuer à l'analyse et la commande de systèmes linéaires dans max-plus en utilisant spécifiquement une approche géométrique. La contribution de cette thèse est centrée sur deux problèmes. La première partie est dédiée à l'étude de la relation entre les notions d'invariance contrôlée et d'invariance contrôlée par retour d'état dynamique dans un semi-anneau. Cette relation permet de montrer l'équivalence de ces deux notions. La deuxième partie concerne un problème original dans la théorie des systèmes linéaires dans max-plus, il s'agit de la synthèse d'une loi de commande par retour d'état, qui permette de satisfaire un ensemble de spécifications exprimées sous la forme de restrictions sur l'état du système, avec une approche géométrique. Il s'agit plus précisément de commander des systèmes à événements discrets décrits par un modèle linéaire dans max-plus. Nous définissons et caractérisons l'ensemble des conditions initiales admissibles, lesquelles sont à l'origine de solutions non décroissantes. Les restrictions temporelles imposées à l'espace d'état du système sont décrites par le semi-module défini par l'image de l'étoile de Kleene de la matrice associée aux restrictions temporelles. Les propriétés géométriques de ce semi-module permettant de garantir que l'évolution du système en boucle fermée satisfasse les restrictions sont étudiées. Des conditions suffisantes concernant l'existence d'une loi de commande causale par retour d'état statique sont présentées. Le calcul des lois de commande causales est également présenté. Pour illustrer l'application de cette approche, deux problèmes de commande sont présentés. / This work is in the context of the theory of linear Systems in the dioids. The initial motivation of this study was to contribute to the analysis and control of max-plus linear systems, specifically using a geometric approach. The contribution of this thesis focuses on two issues. The first part is dedicated to study of the relationship between the concepts of controlled invariance and dynamic state feedback controlled invariance in a semi-ring. This relationship allows us to show the equivalence of these two concepts. The second part relates to a new problem in the theory of max-plus linear systems, it is the synthesis, with a geometric approach, of a static state feedback control law, in order to satisfy a set of specifications that apply to the state space of the system. This is specifically to control of discrete event systems described by a linear model in max-plus. We define and characterize the set of admissible initial conditions, which are the cause of non-decreasing solutions. Temporal restrictions on the system state space are described by the semi-module defined by the image of the Kleene star of the matrix associated with time restrictions. The geometric properties of this semi-module are studied. Sufficient conditions for the existence of a causal control law by static feedback are presented. Calculating causal control laws is also presented. To illustrate the application of this approach, two control problems are presented.

De nos jours, les services Web sont très utilisés notamment par les entreprises pour rendre accessibles leurs métiers, leurs données et leurs savoir-faire via le Web. L'émergence des services Web a permis aux applications d'être présentées comme un ensemble de services métiers bien structurés et correctement décrits, plutôt que comme un ensemble d'objets et de méthodes. La composition automatique de services est une tâche complexe mais qui rend les services interopérables, ainsi leur interaction permet d’offrir une valeur ajoutée dans le traitement des requêtes des utilisateurs en prenant en compte des critères fonctionnels et non fonctionnels de la qualité de service. Dans ce travail de thèse, nous nous intéressons plus précisément aux services à base de localisation (LBS) qui permettent d'intégrer des informations géographiques, et de fournir des informations accessibles depuis des appareils mobiles via, les réseaux mobiles en faisant usage des positions géographiques de ces appareils. L'objectif de ce travail est de proposer une approche orientée modèles pour spécifier, valider et mettre en œuvre des processus de composition automatique de services à des fins de sécurité routière dans les transports. Cette approche est basée sur deux outils formels à savoir les Réseaux de Petri (RdP) et l'algèbre (max,+). Pour cela, nous préconisons l'utilisation des workflow patterns dans la composition, où chaque pattern est traduit par un modèle RdP et ensuite par une équation mathématique dans l'algèbre (max,+). Les modèles formels développés ont conduits, d'une part, à la description graphique et analytique des processus considérés, et d'autre part, à l'évaluation et la vérification quantitatives et qualitatives de ces processus. Une plateforme, appelée TransportML, pour la collaboration et l'interopérabilité de services à base de positionnement a été implémentée. Les résultats obtenus par la simulation des modèles formels sont comparés à ceux issus des simulations du fonctionnement de la plateforme et des expérimentations sur le terrain.Cette thèse est effectuée dans le cadre des projets Européens FP7 ASSET (2008-2011) et TeleFOT (2008-2012). / Web services are widely used by organizations to share their knowledge over the network and facilitate business-to-business collaboration. The emergence of Web services enabled applications to be presented as a set of business services well structured and correctly described. However, combining Web services and making them interoperable, to satisfy user requests taking into account functional and non-functional quality criteria, is a complex process. In this work, we focus specifically on location-based services (LBS) that integrate geographic information and provide information reachable from mobile devices, through wireless network by making use of the geographical positions of the devices. The aim of this work is to develop a model driven approach to specify, validate and implement service composition process in an automatic fashion for road security. This approach is based on two formal tools namely Petri nets (PN) and (max, +) algebra used to model, to verify and to evaluate the performance of service composition process. Workflow patterns are used to represent service composition processes. The behavior of each pattern is modeled by a PN model and then by a (max,+) state equation. The developed formal models allow the graphical and analytical description of the considered processes. Also, these models enable to evaluate some quantitative and qualitative properties of the considered processes. A platform, called TransportML, has been developed for collaboration and interoperability of different LBS. The obtained simulation results from the formal models are compared, on one hand, to those obtained from trials of the platform, and on the other hand, to those obtained from the real experimentations on the field.This work is a part of the FP7 European projects ASSET (2008-2011) and TeleFOT (2008-2012).

Les systèmes de commande en réseau (SCR) sont de plus en plus répandus dans le milieu industriel. Ils procurent en effet de nombreux avantages en termes de coût, de flexibilité, de maintenance, etc. Cependant,l’introduction d’un réseau, qui par nature est composé de ressources partagées, impacte considérablement les performances temporelles des systèmes de commande. Un signal de commande par exemple n’arrive à destination qu’après un certain délai. Pour s’assurer que ce délai soit inférieur à un certain seuil de sécurité ou du respect d’autres contraintes temps réels de ces systèmes, une évaluation au préalable, avant la mise en service d’un SCR, s’avère donc nécessaire. Dans nos travaux de recherche, nous nous intéressons à la réactivité des SCR client/serveur et évaluons leur temps de réponse.Notre contribution dans ces travaux est d’adopter une approche analytique à base de l’algèbre (Max,+) et remédier aux problèmes des méthodes existantes comme l’explosion combinatoire de la vérification formelle ou de la non exhaustivité des approches par simulation. Après modélisation des SCR client/serveur à l’aide de Graphe d’Evénements Temporisés puis représentation de leurs dynamiques à l’aides d’équations (Max,+) linéaires, nous obtenons des formules de calcul direct du temps de réponse. Plus précisément, nous adoptons une analyse déterministe pour calculer les bornes, minimale et maximale, du temps de réponse puis une analyse stochastique pour calculer la fonction de sa distribution. De plus, nous prenons en compte dans nos travaux tous les délais élémentaires qui composent le temps de réponse, y compris les délais de bout-en-bout, dus à la traversée du seul réseau de communication. Ce dernier étant naturellement composé de ressources partagées, rendant l’utilisation des modèles (Max,+) classiques impossibles, nous introduisons une nouvelle approche de modélisation à base du formalisme (Max,+) mais prenant en compte le concept de conflit ou ressource partagée.L’exemple d’un réseau de type Ethernet est considéré pour évaluer ces délais de bout-en-bout. Par ailleurs, cette nouvelle méthode (Max,+) est assez générique et reste applicable à de nombreux systèmes impliquant des ressources partagées, au delà des seuls réseaux de communication. Enfin, pour vérifier la validité des résultats obtenus dans nos travaux, notamment la formule de la borne maximale du temps de réponse, une compagne de mesures expérimentales sont menées sur une plateforme dédiée. Différentes configurations et conditions de trafic dans un réseau Ethernet sont considérées. / Networked automation systems (NAS) are more and more used in industry, given the several advantages they provide like flexibility, low cost, ease of maintenance, etc. However, the use of a communication network in SCR means in essence sharing some resources and therefore strikingly impacts their time performances. For instance, a control signal does get to its destination (actuator) only after a non zero delay. So, to guarantee that such a delay is shorter than a given threshold or other time constraints well respected, an a priori evaluation is necessary before operating the SCR. In our research activities, we are interested in client/server SCR reactivity and the evaluation of their response time.Our contribution in this investigation is the introduction of a (Max,+) Algebra-based analytic approach to solve some problems, faced in the existing methods like state explosion of model checking or the non exhaustivity of simulation. So, after getting Timed Event Graphs based models of the SCR and their linear state (Max,+) representation, we obtain formulae that enables to calculate straightforwardly the SCR response times. More precisely, we obtain formulae of the bounds of response time by adopting a deterministic analysis and other formulae to calculate the probability density of response time by considering a stochastic analysis. Moreover, in our investigation we take into account every single elementary delay involved in the response time, including the end-to-end delays, due exclusively to crossing the communication network. This latter being however constituted of shared resources, making by the way the use of TEG and (Max,+) Algebra impossible, we introduce a novel approach to model the communication network. This approach brings to life a new class of Petri nets, called Conflicting Timed Event Graphs (CTEG), which enables us to solve the problem of the shared resources. We also manage to represent the CTEG dynamics using recurrent (Max,+) equations and therefore calculate the end to-end delays. An Ethernet-based network is studied as an example to apply this novel approach. Note by the way that the field of application of this approach borders largely communication networks and is quite possible when dealing with other systems.Finally, to validate the different results of our research activities and the related hypotheses, especially the maximal bound of response time formula, we carry out lots of experimental measurements on a lab facility. We compare the measures to the formula predictions and check their agreement under different conditions.

Les Systèmes à Evénements Discrets (SED) peuvent être définis comme des systèmes dans lesquels les variables d'état changent sous l'occurrence d'évènements au fil du temps. Les SED mettant en jeu des phénomènes de synchronisation peuvent être modélisés par des équations linéaires dans les algèbres de type (max,+). L'analyse d'atteignabilité est une problématique majeure pour les systèmes dynamiques. L'objectif est de calculer l'ensemble des états atteignables d'un système dynamique pour toutes les valeurs admissibles d'un ensemble d'états initiaux. Le problème de l'analyse d'atteignabilité pour les systèmes Max-Plus Linéaire (MPL) a été, proprement, résolu en décomposant le système MPL en une combinaison de systèmes affines par morceaux où les composantes affines du système sont représentées par des matrices de différences bornées (Difference Bound Matrix, DBM). La contribution principale de cette thèse est de présenter une procédure similaire pour résoudre le problème de l'atteignabilité pour des systèmes MPL incertains (uMPL), c'est-à-dire des systèmes MPL soumis à des bruits bornés, des perturbations et/ou des erreurs de modélisation. Tout d'abord, nous présentons une procédure permettant de partionner l'espace d'état d'un système uMPL en parties représentables par des DBM. Ensuite, nous étendons l'analyse d'atteignabilité des systèmes MPL aux systèmes uMPL. Enfin, les résultats sur l'analyse d'atteignabilité sont mis en oeuvre pour résoudre le problème d'atteignabilité conditionnelle, qui est étroitement lié au calcul du support de la densité de probabilité impliquée dans le problème de filtage stochastique / Discrete Event Dynamic Systems (DEDS) are discrete-state systems whose dynamics areentirely driven by the occurrence of asynchronous events over time. Linear equations in themax-plus algebra can be used to describe DEDS subjected to synchronization and time delayphenomena. The reachability analysis concerns the computation of all states that can bereached by a dynamical system from an initial set of states. The reachability analysis problemof Max Plus Linear (MPL) systems has been properly solved by characterizing the MPLsystems as a combination of Piece-Wise Affine (PWA) systems and then representing eachcomponent of the PWA system as Difference-Bound Matrices (DBM). The main contributionof this thesis is to present a similar procedure to solve the reachability analysis problemof MPL systems subjected to bounded noise, disturbances and/or modeling errors, calleduncertain MPL (uMPL) systems. First, we present a procedure to partition the state spaceof an uMPL system into components that can be completely represented by DBM. Then weextend the reachability analysis of MPL systems to uMPL systems. Moreover, the results onreachability analysis of uMPL systems are used to solve the conditional reachability problem,which is closely related to the support calculation of the probability density function involvedin the stochastic filtering problem. / Os Sistemas a Eventos Discretos (SEDs) constituem uma classe de sistemas caracterizada por apresentar espaço de estados discreto e dinâmica dirigida única e exclusivamente pela ocorrência de eventos. SEDs sujeitos aos problemas de sincronização e de temporização podem ser descritos em termos de equações lineares usando a álgebra max-plus. A análise de alcançabilidade visa o cálculo do conjunto de todos os estados que podem ser alcançados a partir de um conjunto de estados iniciais através do modelo do sistema. A análise de alcançabilidade de sistemas Max Plus Lineares (MPL) pode ser tratada por meio da decomposição do sistema MPL em sistemas PWA (Piece-Wise Affine) e de sua correspondente representação por DBM (Difference-Bound Matrices). A principal contribuição desta tese é a proposta de uma metodologia similar para resolver o problema de análise de alcançabilidade em sistemas MPL sujeitos a ruídos limitados, chamados de sistemas MPL incertos ou sistemas uMPL (uncertain Max Plus Linear Systems). Primeiramente, apresentamos uma metodologia para particionar o espaço de estados de um sistema uMPL em componentes que podem ser completamente representados por DBM. Em seguida, estendemos a análise de alcançabilidade de sistemas MPL para sistemas uMPL. Além disso, a metodologia desenvolvida é usada para resolver o problema de análise de alcançabilidade condicional, o qual esta estritamente relacionado ao cálculo do suporte da função de probabilidade de densidade envolvida o problema de filtragem estocástica.