Cette thèse cherche à résoudre en pratique le problème de couverture dans les réseaux de Petri et les systèmes de canaux à pertes (LCS). Ces systèmes sont intéressants à étudier car ils permettent de modéliser facilement les systèmes concurrents et les systèmes distribués. Le problème de couverture dans un système de transitions consiste à savoir si on peut, à partir d’un état initial arriver à un état plus grand qu’un état cible. La résolution de ce problème dans les systèmes de transitions bien structurés (WSTS) sera le sujet d’études de la première partie. Les réseaux de Petri et les LCS sont des WSTS. On donnera dans la première partie une méthode générale pour le résoudre rapidement en pratique. Cette méthode utilise des invariants de couverture, qui sont des sur-approximations de l’ensemble des états couvrables. La seconde partie sera consacrée aux réseaux de Petri. Elle présentera diverses comparaisons théoriques et pratiques de différents invariants de couverture. Nous nous intéresserons notamment à la combinaison de l’invariant classique de l’inéquation d’état avec une analyse de signe simple. Les LCS seront le sujet d’études de la troisième partie. On présentera une variante de l’inéquation d’état adaptée aux LCS ainsi que deux invariants qui retiennent des propriétés sur l’ordre dans lequel les messages sont envoyés. La thèse a mené à la création de deux outils, ICover et BML, pour résoudre le problème de couverture respectivement dans les réseaux de Petri et dans les LCS. / The goal of this thesis is to solve in practice the coverability problem in Petri nets and lossy channel systems (LCS). These systems are interesting to study because they can be used to model concurrent and distributed systems. The coverability problem in a transition system is to decide whether it is possible, from an initial state, to reach a greater state than a target state. In the first part, we discuss how to solve this problem for well-structured transition systems (WSTS). Petri nets and LCS are WSTS. In the first part, we present a general method to solve this problem quickly in practice. This method uses coverability invariants, which are over-approximations of the set of coverable states. The second part studies Petri nets.We present comparisons of coverability invariants, both in theory and in practice. A particular attention will be paid on the combination of the classical state inequation and a simple sign analysis. LCS are the focus of the third part. We present a variant of the state inequation for LCS and two invariants that compute properties for the order in which messages are sent. Two tools, ICover and BML, were developed to solve the coverability problem in Petri nets and LCS respectively.

Les langages de représentation de connaissances (LRCs) sont des langages qui permettent de représenter et partager des informations sous une forme logique. Il y a de nombreux LRCs. Chaque LRC a un modèle structurel abstrait et peut avoir plusieurs notations. Ces modèles et notations ont été conçus pour répondre à des besoins de modélisation ou de calculabilité différents, ainsi qu'à des préférences différentes. Les outils actuels gérant ou traduisant des RCs ne travaillent qu'avec quelques LRCs et ne permettent pas – ou très peu – à leurs utilisateurs finaux d'adapter les modèles et notations de ces LRCs. Cette thèse contribue à résoudre ces problèmes pratiques et le problème de recherche original suivant : “une fonction d'import et une fonction d'export de RCs peuvent-elle être spécifiées de façon générique et, si oui, comment leurs ressources peuvent-elles êtres spécifiées ?”. Cette thèse s'inscrit dans un projet plus vaste dont l'objectif général est de faciliter le partage et la réutilisation des connaissances liées aux composants logiciels et à leurs présentations. L'approche suivie dans cette thèse est basée sur une ontologie de LRCs nommée KRLO, et donc sur une représentation formelle de ces LRCs.KRLO a trois caractéristiques importantes et originales auxquelles cette thèse à contribué : i) elle représente des modèles de LRCs de différentes familles de façon uniforme, ii) elle inclut une ontologie de notations de LRCs, et iii) elle spécifie des fonctions génériques pour l'import et l'export de RCs dans divers LRCs. Cette thèse a contribué à améliorer la première version de KRLO (KRLO_2014) et à donner naissance à sa seconde version. KRLO_2014 contenait des imprécisions de modélisation qui rendaient son exploitation difficile ou peu pratique. Cette thèse a aussi contribué à la spécification et l'opérationnalisation de “Structure_map”, une fonction permettant d'écrire de façon modulaire et paramétrable toute autre fonction utilisant une boucle. Son utilisation permet de créer et d'organiser les fonctions en une ontologie de composants logiciels. Pour implémenter une fonction générique d'export basée sur KRLO, j'ai développé SRS (Structure_map based Request Solver), un résolveur d'expressions de chemins sur des RCs. SRS interprète toutes les fonctions. SRS apporte ainsi une validation expérimentale à la fois à l'utilisation de cette primitive (Structure_map) et à l'utilisation de KRLO. Directement ou indirectement, SRS et KRLO pourront être utilisés par GTH (Global Technologies Holding), l'entreprise partenaire de cette thèse. / Knowledge Representation Languages (KRLs) are languages enabling to represent and share information in a logical form. There are many KRLs. Each KRL has one abstract structural model and can have multiple notations. These models and notations were designed to meet different modeling or computational needs, as well as different preferences. Current tools managing or translating knowledge representations (KRs) allow the use of only one or few KRLs and do not enable – or hardly enable – their end-users to adapt the models and notations of these KRLs. This thesis helps to solve these practical problems and this original research problem: “Can a KR import function and a KR export function be specified in a generic way and, if so, how can their resources be Specified ?”. This thesis is part of a larger project the overall objective of which is to facilitate i) the sharing and reuse of knowledge related to software components, and ii) knowledge presentations. The approach followed in this thesis is based on an ontology of KRLs named KRLO, and therefore on a formal representation of these KRLs.KRLO has three important and original features to which this thesis contributed: i) it represents KRL models of different families in a uniform way, ii) it includes an ontology of KRLs notations, and iii) it specifies generic functions for KR import and export in various KRLs. This thesis has contributed to the improvement of the first version of KRLO (KRLO_2014) and to the creation of its second version. KRLO_2014 contained modeling inaccuracies that made it difficult or inconvenient to use. This thesis has also contributed to the specification and the operationalization of “Structure_map”, a function enabling to write any other function that uses a loop, in a modular and configurable way. Its use makes it possible to create and organize these functions into an ontology of software components. To implement a generic export function based on KRLO, I developed SRS (Structure_map based Request Solver), a KR retrieval tool enabling the use of KR path expressions. SRS interprets all functions. SRS thus provides an experimental validation for both the use of this primitive (Structure_map) and the use of KRLO.Directly or indirectly, SRS and KRLO may be used by GTH (Global Technologies Holding), the partner company of this thesis.

La vérification de logiciels repose le plus souvent sur une spécification formelle encodant les propriétés du programme à vérifier. La tâche de spécification et de vérification déductive des programmes est longue et difficile et nécessite une connaissance des outils de preuve de programmes. En effet, un échec de preuve de programme peut être dû à une non-conformité du code par rapport à sa spécification, à un contrat de boucle ou de fonction appelée trop faible pour prouver une autre propriété, ou à une incapacité du prouveur. Il est souvent difficile pour l’utilisateur de décider laquelle de ces trois raisons est la cause de l’échec de la preuve car cette information n’est pas (ou rarement) donnée par le prouveur et requiert donc une revue approfondie du code et de la spécification. L’objectif de cette thèse est de fournir une méthode de diagnostic automatique des échecs de preuve afin d’améliorer le processus de spécification et de preuve des programmes C. Nous nous plaçons dans le cadre de la plate-forme d’analyse des programmes C FRAMA-C, qui fournit un langage de spécification unique ACSL, un greffon de vérification déductive WP et un générateur de tests structurels PATHCRAWLER. La méthode que nous proposons consiste à diagnostiquer les échecs de preuve en utilisant la génération de tests structurels sur une version instrumentée du programme d’origine / Software verification often relies on a formal specification encoding the program properties to check. Formally specifying and deductively verifying programs is difficult and time consuming and requires some knowledge about theorem provers. Indeed, a proof failure for a program can be due to a noncompliance between the code and its specification, a loop or callee contrat being insufficient to prove another property, or a prover incapacity. It is often difficult for the user to decide which one of these three reasons causes a given proof failure. Indeed, this feedback is not (or rarely) provided by the theorem prover thus requires a thorough review of the code and the specification. This thesis develops a method to automatically diagnose proof failures and facilitate the specification and verification task. This work takes place within the analysis framework for C programs FRAMAC, that provides the specification language ACSL, the deductive verification plugin WP, and the structural test generator PATHCRAWLER. The proposed method consists in diagnosing proof failures using structural test generation on an instrumented version of the program under verification.

Cette thèse étudie l’enforcement de propriétés temporisées à l’exécution en présence d’évènements incontrôlables. Les travaux se placent dans le cadre plus général de la vérification à l’exécution qui vise à surveiller l’exécution d’un système afin de s’assurer qu’elle respecte certaines propriétés. Ces propriétés peuvent être spécifiées à l’aide de formules logiques, ou au moyen d’autres modèles formels, parfois équivalents, comme des automates. Nous nous intéressons à l’enforcement à l’exécution de propriétés spécifiées par des automates temporisés. Tout comme la vérification à l’exécution, l’enforcement à l’exécution surveille l’exécution d’un système, la différence étant qu’un mécanisme d’enforcement réalise certaines modifications sur l’exécution afin de la contraindre à satisfaire la propriété souhaitée. Nous étudions plus particulièrement l’enforcement à l’exécution lorsque certains évènements de l’exécution sont incontrôlables, c’est-à-dire qu’ils ne peuvent pas être modifiés par un mécanisme d’enforcement. Nous définissons des algorithmes de synthèse de mécanismes d’enforcement décrits de manières fonctionnelle puis opérationnelle, à partir de propriétés temporisées régulières (pouvant être représentées par des automates temporisés). Ainsi, deux mécanismes d’enforcement équivalents sont définis, le premier présentant une approche correcte sans considération d’implémentation, alors que le second utilise une approche basée sur la théorie des jeux permettant de précalculer certains comportements, ce qui permet de meilleures performances. Une implémentation utilisant ce précalcul est également présentée et évaluée. Les résultats sont encourageant quant à la faisabilité de l’enforcement à l’exécution en temps réel, avec des temps supplémentaires suffisamment courts sur de petites propriétés pour permettre une utilisation de tels systèmes. / This thesis studies the runtime enforcement of timed properties when some events are uncontrollable. This work falls in the domain of runtime verification, which includes all the techniques and tools based on or related to the monitoring of system executions with respect to requirement properties. These properties can be specified using different models such as logic formulae or automata. We consider timed regular properties, that can be represented by timed automata. As for runtime verification, a runtime enforcement mechanism watches the executions of a system, but instead of just outputting a verdict, it modifies the execution so that it satisfies the property. We are interested in runtime enforcement with uncontrollable events. An uncontrollable event is an event that an enforcement mechanism can not modify. We describe the synthesis of enforcement mechanisms, in both a functional and an operational way, that enforce some desired timed regular property. We define two equivalent enforcement mechanisms, the first one being simple, without considering complexity aspects, whereas the second one has a better time complexity thanks to the use of game theory; the latter being better suited for implementation. We also detail a tool that implements the second enforcement mechanism, as well as some performance considerations. The overhead introduced by the use of our tool seems low enough to be used in some real-time application scenarios.

Nous avons développé dans le cadre de cette thèse deux aspects complémentaires liés à la sécurité des systèmes d’agents mobiles : l'aspect statique et l'aspect dynamique. Pour l’aspect statique, nous avons proposé une spécification formelle des politiques de sécurité qui traite les différentes préoccupations de sécurité dans les systèmes à base d'agents mobiles et couvre les différents concepts liés à la définition de tels systèmes. L'aspect dynamique, s'intéresse à définir formellement l'ensemble des opérations élémentaires de reconfiguration de ces politiques et de définir un cadre qui exprime l'adaptabilité de la politique de l'agent aux nouvelles exigences de sécurité du système visité. Pour les deux aspects, nous avons porté un intérêt considérable à la vérification formelle. Les démarches de vérification élaborées sont implémentées et validées sous l'outil de preuve Z/EVES. D’un point de vue opérationnel, nous avons défini un cadre pour l'imposition des politiques de sécurité. Ce dernier tire profit du cadre théorique, que nous avons défini, et applique une approche de génération de code basée sur le paradigme de la POA. / We develop two complementary aspects related to the security of mobile agent systems: the static and dynamic aspect. The first is related to the specification of security policies which treats the various security concerns in mobile agent systems and covers the various concepts related to the modeling of such systems. The dynamic aspect takes an interest to define a set of elementary operations which may change a given policy and a framework that expresses the adaptability of the agent policy to the security requirements of the new visited system. All Specifications are coded in Z notation.Another main contribution consists in providing a formal verification framework which gives more completeness and more consistency to the proposed specifications for both aspects. All checking processes are implemented under the Z/EVES theorem prover. Finally, we have take advantage from this theoretical work and we have defined an operational framework for enforcement security policies which combine the strengths of AOP with those of formal methods.

Cette thèse présente une extension du compilateur CompCert permettant de fournir des garanties formelles de préservation sémantique à des programmes auxquels CompCert n'en donne pas. CompCert est un compilateur pour le langage C vers différentes architectures qui fournit, en plus d'un exécutable compilé, des garanties formelles concernant le comportement du programme assembleur généré. En particulier, tout programme C ayant une sémantique définie selon le standard C est compilé en un programme assembleur équivalent, c'est-à-dire qui a la même sémantique. En revanche, ce théorème n'assure aucune garantie lorsque le programme source n'a pas de sémantique définie : on parle en C de comportement indéfini. Toutefois, des programmes C issus de réels projets largement utilisés contiennent des comportements indéfinis. Cette thèse détaille dans un premier temps un certain nombre d'exemples de programmes C qui déclenchent des comportements indéfinis. Nous argumentons que ces programmes devraient tout de même bénéficier du théorème de préservation sémantique de CompCert, d'abord parce qu'ils apparaissent dans de vrais projets et parce que leur utilisation des comportements indéfinis semble légitime. Dans ce but, nous proposons d'abord un modèle mémoire pour CompCert qui définit l'arithmétique arbitraire de pointeurs et la manipulation de données non initialisées, à l'aide d'un formalisme de valeurs symboliques qui capturent la sémantique d'opérations non définies dans le standard. Nous adaptons l'intégralité du modèle mémoire de CompCert avec ces valeurs symboliques, puis nous adaptons les sémantiques formelles de chacun des langages intermédiaires de CompCert. Nous montrons que ces sémantiques symboliques sont un raffinement des sémantiques existantes dans CompCert, et nous montrons par ailleurs que ces sémantiques capturent effectivement le comportement des programmes sus-cités. Enfin, afin d'obtenir des garanties similaires à celles que CompCert fournit, nous devons adapter les preuves de préservation sémantique à notre nouveau modèle. Pour ce faire, nous généralisons d'importantes techniques de preuves comme les injections mémoire, ce qui nous permet de transporter les preuves de CompCert sur nos nouvelles sémantiques. Nous obtenons ainsi un théorème de préservation sémantique qui traite plus de programmes C. / This thesis presents an extension of the CompCert compiler that aims at providing formal guarantees about the compilation of more programs than CompCert does. The CompCert compiler compiles C code into assembly code for various architectures and provides formal guarantees about the behaviour of the compiled assembly program. It states that whenever the C program has a defined semantics, the generated assembly program behaves similarly. However, the theorem does not provide any guarantee when the source program has undefined semantics, or, in C parlance, when it exhibits undefined behaviour, even though those behaviours actually happen in real-world code. This thesis exhibits a number of C idioms, that occur in real-life code and whose behaviour is undefined according to the C standard. Because they happen in real programs, our goal is to enhance the CompCert verified compiler so that it also provides formal guarantees for those programs. To that end, we propose a memory model for CompCert that makes pointer arithmetic and uninitialised data manipulation defined, introducing a notion of symbolic values that capture the meaning of otherwise undefined idioms. We adapt the whole memory model of CompCert with this new formalism and adapt the semantics of all the intermediate languages. We prove that our enhanced semantics subsumes that of CompCert. Moreover, we show that these symbolic semantics capture the behaviour of the previously undefined C idioms. The proof of semantic preservation from CompCert needs to be reworked to cope with our model. We therefore generalize important proof techniques such as memory injections, which enable us to port the whole proof of CompCert to our new memory model, therefore providing formal guarantees for more programs.

Ce travail de thèse propose une nouvelle approche au traitement des langues naturelles. Plutôt qu'essayer d'estimer directement la probabilité d'une phrase quelconque, nous identifions des structures syntaxiques dans le langage, qui peuvent être utilisées pour modifier et créer de nouvelles phrases à partir d'un échantillon initial. L'étude des structures syntaxiques est accomplie avec des ensembles de substitution Markoviens, ensembles de chaînes de caractères qui peuvent être échangées sans affecter la distribution. Ces ensembles définissent des processus de substitution Markoviens qui modélisent l'indépendance conditionnelle de certaines chaînes vis-À-Vis de leur contexte. Ce point de vue décompose l'analyse du langage en deux parties, une phase de sélection de modèle, où les ensembles de substitution sont sélectionnés, et une phase d'estimation des paramètres, où les fréquences pour chaque ensemble sont estimées. Nous montrons que ces processus constituent des familles exponentielles quand la structure du langage est fixée. Lorsque la structure du langage est inconnue, nous proposons des méthodes pour identifier des ensembles de substitution à partir d'un échantillon, et pour estimer les paramètres de la distribution. Les ensembles de substitution ont quelques relations avec les grammaires hors-Contexte, qui peuvent être utilisées pour aider l'analyse. Nous construisons alors des dynamiques invariantes pour les processus de substitution. Elles peuvent être utilisées pour calculer l'estimateur du maximum de vraisemblance. En effet, les processus de substitution peuvent être vus comme la limite thermodynamique de la mesure invariante d'une dynamique de crossing-Over. / This thesis proposes a new approach to natural language processing. Rather than trying to estimate directly the probability distribution of a random sentence, we will detect syntactic structures in the language, which can be used to modify and create new sentences from an initial sample.The study of syntactic structures will be done using Markov substitute sets, sets of strings that can be freely substituted in any sentence without affecting the whole distribution. These sets define the notion of Markov substitute processes, modelling conditional independence of certain substrings (given by the sets) with respect to their context. This point of view splits the issue of language analysis into two parts, a model selection stage where Markov substitute sets are selected, and a parameter estimation stage where the actual frequencies for each set are estimated.We show that these substitute processes form exponential families of distributions, when the language structure (the Markov substitute sets) is fixed. On the other hand, when the language structure is unknown, we propose methods to identify Markov substitute sets from a statistical sample, and to estimate the parameters of the distribution. Markov substitute sets show some connections with context-Free grammars, that can be used to help the analysis. We then proceed to build invariant dynamics for Markov substitute processes. They can among other things be used to effectively compute the maximum likelihood estimate. Indeed, Markov substitute models can be seen as the thermodynamical limit of the invariant measure of crossing-Over dynamics.

Les systèmes hybrides sont au cœur des systèmes cyber-physiques. De tels systèmes représentent l’interaction de processus physiques continus modélisant généralement l'environnement avec des décisions discrètes issues d'un système de contrôle commande électronique. La vérification de ces systèmes est cruciale pour assurer leur sûreté dès la phase de modélisation. Les recherches sur les systèmes hybrides ont de nombreux domaines d’application, notamment le transport, l’aéronautique et la biologie. La thèse étudie des principes du raisonnement qualitatif et les applique à la vérification des systèmes hybrides. Le travail consiste à élaborer une méthode pour abstraire le système hybride en utilisant des principes qualitatifs. On recourt à une discrétisation finie de l'espace d'état tout en conservant des caractéristiques qualitatives du système. L'abstraction calculée permet de prouver des propriétés au niveau du système hybride concret et fournit une représentation du comportement global du système. Un outil développé en C++ permet de calculer l'abstraction d'un système hybride donné. Une évaluation de ses performances est établie. On s'intéresse particulièrement à une propriété de sûreté des systèmes appelée diagnosticabilité. Un modèle de système est dit diagnosticable s'il permet d'identifier sans ambiguïté la survenue de toute faute modélisée à partir des seules observations disponibles du système jusqu’à un certain délai après l’occurrence de la faute. Une méthode qui consiste à utiliser l'abstraction établie précédemment pour vérifier la diagnosticabilité d'un système hybride est proposée. / Hybrid systems are at the core of cyber-physical systems. Such systems represent the interaction between continuous physical processes generally modelling the environment with discrete decisions from control electronic signaling. The verification of these systems is crucial to ensure safety at the modeling stage. The application of hybrid systems is present in many fields such as transportation, biology and avionics. The thesis studies principals from the qualitative reasoning domain and applies them to the verification of hybrid systems. The accomplished work elaborates methods to abstract a hybrid system using qualitative principles. These methods consist in discretizing the state space to a finite number of states while conserving qualitative characteristics. The computed abstraction allows to prove properties at the level of the concrete hybrid system and presents a representation of the global behavior of the system. A tool developed in C++ computes the abstraction of a given hybrid system. An evaluation of its performance is performed. We are also interested in a particular property called diagnosability. The system is said to be diagnosable when it is capable to identify modeled faults using limited specified observations. A method that uses the computed abstraction to verify diagnosability of a given hybrid system is proposed.

Les réseaux MANET représentent un domaine important de recherche en raison des nombreuses opportunités découlant des problématiques et des applications inhérentes à ce type de réseau. Les problématiques les plus récurrentes sont la mobilité, la disponibilité ainsi que les ressources limitées. Un intérêt bien connu dans les réseaux et donc dans les MANET est de monitorer les propriétés de ce réseau et de ses nœuds. Les contraintes des MANET peuvent avoir un impact significatif sur les efforts mis en œuvre pour les monitorer. La mobilité et la disponibilité peuvent créer des résultats incomplets pour le monitorage. Les propriétés usuelles utilisées en monitorage sont simples, comme notamment la consommation moyenne du processeur, la bande passante moyenne, etc. De plus, l'évolution des réseaux a conduit à un besoin croissant d'examiner des comportements plus complexes, dépendants et imbriqués. La littérature indique que la précision des valeurs obtenues par monitorage et donc des approches n'est pas fiable et difficile à atteindre en raison des propriétés dynamiques du MANET. Nous proposons donc des architectures de surveillance décentralisées et distribuées qui reposent sur de multiples points d'observation. L'approche décentralisée combine des algorithmes dits hiérarchiques et de ‘gossip’ pour fournir une approche de monitorage efficace. Grâce à des expérimentations approfondies, nous avons conclu que même si nous étions en mesure d'atteindre d’excellentes performances, la fragmentation du réseau a toujours un impact sévère sur la méthodologie mise en place. Essayant d'améliorer notre technique, nous avons proposé une approche distribuée pour améliorer l'efficacité et la précision globale.Il fournit un mécanisme de consensus qui lui permet d'agréger de nombreux résultats fournis par plusieurs nœuds et fournit un résultat plus significatif et plus précis. Nous soutenons notre proposition avec de nombreuses définitions mathématiques qui modélisent les résultats locaux pour un seul nœud et les résultats globaux pour le réseau. Nos expériences ont été évaluées avec un émulateur construit en interne qui s'appuie sur Amazon Web Services, NS-3, Docker et GoLang avec un nombre variable de nœuds, la taille du réseau, sa densité, la vitesse des nœuds, les algorithmes de mobilité et les délais. Grâce à cet émulateur, nous avons pu analyser plusieurs aspects en fournissant des testbeds reproductibles, documentés et accessibles. Nous avons obtenu des résultats prometteurs pour les deux approches, et surtout pour l'approche distribuée en particulier en ce qui concerne la précision des valeurs obtenues par monitorage / MANETs represent a significant area of network research due to the many opportunities derived from the problematics and applications. The most recurring problematics are the mobility, the availability and also the limited resources. A well-known interest in networks and therefore in MANETs is to monitor properties of the network and nodes. The problematics of the MANETs can have a significant impact on the monitoring efforts. Mobility and availability can create incomplete results for the monitoring. The usual properties discussed in monitoring are simple ones, e.g., average CPU consumption, average bandwidth and so on. Moreover, the evolution of networks has led to an increasing need to examine more complex, dependent and intertwined behaviors. The literature states that accuracy of the approaches is not reliable and difficult to achieve due to the dynamic properties of the MANET. Therefore, we propose a decentralized and distributed monitoring architecture that rely on multiple points of observation. The decentralized approach combines gossip and hierarchical algorithms to provide an effective monitoring approach. Through extensive experimentation, we concluded that although we were able to achieve exceptional performance, network fragmentation still has a harsh impact on the approach. Trying to improve our approach, we proposed a distributed approach, relying on stronger bedrock to enhance the overall efficiency and accuracy. It provides a consensus mechanism that allows it to aggregate and provides a more meaningful and accurate result. We support our proposal with numerous mathematical definition that models local results for a single node and global results for the network. Our experiments were evaluated with an emulator built in-house that relies on Amazon Web Services, NS-3, Docker and GoLang with varying number of nodes, network size, network density, speed, mobility algorithms and timeouts. Through this emulator, we were able to analyze multiple aspects of the approaches by providing a repeatable, documented and accessible test beds. We obtained promising results for both approaches, but for the distributed approach, especially regarding accuracy

Dans un contexte applicatif de surveillance de zone maritime, nous voulons fournir à un opérateur humain des informations sémantiquement riches et dynamiques relatives aux comportements des entités sous surveillance. Réussir à relier les mesures brutes en provenance d’un système de capteurs aux descriptions abstraites de ces comportements est un problème difficile. Ce dernier est d’ailleurs en général traité en deux temps: tout d’abord, réaliser un prétraitement sur les données hétérogènes, multidimensionnelles et imprécises pour les transformer en un flux d’évènements symbolique, puis utiliser des techniques de reconnaissance de plans sur ces mêmes évènements. Ceci permet de décrire des étapes de plans symboliques de haut niveau sans avoir à se soucier des spécificités des capteurs bas niveau. Cependant, cette première étape est destructrice d’information et de ce fait génère une ambigüité supplémentaire dans le processus de reconnaissance. De plus, séparer les tâches de reconnaissance de comportements est générateur de calculs redondants et rend l’écriture de la bibliothèque de plans plus ardue. Ainsi, nous proposons d’aborder cette problématique sans séparer en deux le processus de reconnaissance. Pour y parvenir, nous proposons un nouveau modèle hiérarchique, inspiré de la théorie des langages formels, nous permettant de construire un pont au-dessus du fossé sémantique séparant les mesures des capteurs des intentions des entités. Grâce à l’aide d’un ensemble d’algorithmes manipulant ce modèle, nous sommes capables, à partir d’observations, de déduire les plausibles futures évolutions de la zone sous surveillance, tout en les justifiant des explications nécessaires. / In a maritime area supervision context, we seek providing a human operator with dynamic information on the behaviors of the monitored entities. Linking raw measurements, coming from sensors, with the abstract descriptions of those behaviors is a tough challenge. This problem is usually addressed with a two-stepped treatment: filtering the multidimensional, heterogeneous and imprecise measurements into symbolic events and then using efficient plan recognition techniques on those events. This allows, among other things, the possibility of describing high level symbolic plan steps without being overwhelmed by low level sensor specificities. However, the first step is information destructive and generates additional ambiguity in the recognition process. Furthermore, splitting the behavior recognition task leads to unnecessary computations and makes the building of the plan library tougher. Thus, we propose to tackle this problem without dividing the solution into two processes. We present a hierarchical model, inspired by the formal language theory, allowing us to describe behaviors in a continuous way, and build a bridge over the semantic gap between measurements and intents. Thanks to a set of algorithms using this model, we are able, from observations, to deduce the possible future developments of the monitored area while providing the appropriate explanations.