Dans cette thèse, nous considérons deux problèmes auxquels le model checking statistique doit faire face. Le premier concerne les systèmes hétérogènes qui introduisent complexité et non-déterminisme dans l'analyse. Le second problème est celui des propriétés rares, difficiles à observer et donc à quantifier. Pour le premier point, nous présentons des contributions originales pour le formalisme des systèmes composites dans le langage BIP. Nous en proposons une extension stochastique, SBIP, qui permet le recours à l'abstraction stochastique de composants et d'éliminer le non-déterminisme. Ce double effet a pour avantage de réduire la taille du système initial en le remplaçant par un système dont la sémantique est purement stochastique sur lequel les algorithmes de model checking statistique sont définis. La deuxième partie de cette thèse est consacrée à la vérification de propriétés rares. Nous avons proposé le recours à un algorithme original d'échantillonnage préférentiel pour les modèles dont le comportement est décrit à travers un ensemble de commandes. Nous avons également introduit les méthodes multi-niveaux pour la vérification de propriétés rares et nous avons justifié et mis en place l'utilisation d'un algorithme multi-niveau optimal. Ces deux méthodes poursuivent le même objectif de réduire la variance de l'estimateur et le nombre de simulations. Néanmoins, elles sont fondamentalement différentes, la première attaquant le problème au travers du modèle et la seconde au travers des propriétés. / In this thesis, we consider two problems that statistical model checking must cope. The first problem concerns heterogeneous systems, that naturally introduce complexity and non-determinism into the analysis. The second problem concerns rare properties, difficult to observe, and so to quantify. About the first point, we present original contributions for the formalism of composite systems in BIP language. We propose SBIP, a stochastic extension and define its semantics. SBIP allows the recourse to the stochastic abstraction of components and eliminate the non-determinism. This double effect has the advantage of reducing the size of the initial system by replacing it by a system whose semantics is purely stochastic, a necessary requirement for standard statistical model checking algorithms to be applicable. The second part of this thesis is devoted to the verification of rare properties in statistical model checking. We present a state-of-the-art algorithm for models described by a set of guarded commands. Lastly, we motivate the use of importance splitting for statistical model checking and set up an optimal splitting algorithm. Both methods pursue a common goal to reduce the variance of the estimator and the number of simulations. Nevertheless, they are fundamentally different, the first tackling the problem through the model and the second through the properties.

La maintenance de flottes de systèmes mobiles dans le monde du transport et de la logistique revêt de nos jours une importance croissante de par l’augmentation des attentes des exploitants et opérateurs en termes de sécurité, de fiabilité, de suivi, de diagnostic et de maintenance de ces systèmes. Dans ce contexte, Les mainteneurs des flottes doivent souvent faire face à d'énormes quantités de données brutes, informations et événements de surveillance liés aux contexte de leurs systèmes. De plus, ces événements, données et informations manquent souvent de précision et sont souvent contradictoires ou obsolètes. Enfin, le degré d'urgence des décisions de maintenance est rarement pris en compte. Ce travail est consacré à la proposition et à la mise au point d’une architecture de surveillance pour l’aide à la maintenance d’une flotte de systèmes mobiles. Cette architecture, appelée EMH², est destinée à faciliter le diagnostic et le suivi de ce type de flotte. Elle est construite sur les principes holoniques, des plus bas (capteurs) aux plus hauts niveaux (ensemble d’une flotte de systèmes mobiles). Elle se base également sur une standardisation des événements traités afin de traiter les données de manière générique. Cette architecture, indépendante des types de systèmes surveillés et de leur niveau hiérarchique, peut devenir l'épine dorsale d’une stratégie efficace de maintenance proactive d’une flotte. Une méthodologie de déploiement est ainsi proposée. Une étude en simulation et une application sur une flotte de 10 trains actuellement en service est présentée. / The maintenance of mobile systems fleets in the world of transport and logistics is of increasing importance today due to the increasing expectations of operators in terms of safety, reliability, monitoring, diagnosis and maintenance of these systems. In this context, fleet maintainers often have to deal with huge amounts of raw data, information and monitoring events related to the context of their systems. Moreover, these events, data and information are often lack precision and often contradictory or obsolete. Finally, the urgency of maintenance decisions is rarely taken into account. This work is devoted to the proposal and the development of a monitoring architecture to help maintain a fleet of mobile systems. This architecture, called EMH², is intended to facilitate the diagnosis and monitoring of this type of fleet. It is built on holonic principles, from the lowest (sensors) to the highest levels (a whole fleet of mobile systems). It is also based on a standardization of processed events in order to process the data generically. This architecture, independent of the types of systems monitored and their hierarchical level, can become the backbone of an effective strategy for proactive fleet maintenance. A deployment methodology is thus proposed. A simulation study and an application on a fleet of 10 trains currently in service is presented.

Notre société est de plus en plus présente sur le Web. En conséquence, une grande partie des événements quotidiens a vocation à être numérisée. Dans ce cadre, le Web contient des descriptions de divers événements du monde réel et provenant du monde entier. L'ampleur de ces événements peut varier, allant de ceux pertinents uniquement localement à ceux qui retiennent l'attention du monde entier. La presse et les médias sociaux permettent d’atteindre une diffusion presque mondiale. L’ensemble de toutes ces données décrivant des événements sociétaux potentiellement complexes ouvre la porte à de nombreuses possibilités de recherche pour analyser et mieux comprendre l'état de notre société.Dans cette thèse, nous étudions diverses tâches d’analyse de l’impact des événements sociétaux. Plus précisément, nous abordons trois facettes dans le contexte des événements et du Web, à savoir la diffusion d’événements dans des communautés de langues étrangères, la classification automatisée des contenus Web et l’évaluation et la visualisation de la viralité de l’actualité. Nous émettons l'hypothèse que les entités nommées associées à un événement ou à un contenu Web contiennent des informations sémantiques précieuses, qui peuvent être exploitées pour créer des modèles de prédiction précis. À l'aide de nombreuses études, nous avons montré que l'élévation du contenu Web au niveau des entités saisissait leur essence essentielle et offrait ainsi une variété d'avantages pour obtenir de meilleures performances dans diverses tâches. Nous exposons de nouvelles découvertes sur des tâches disparates afin de réaliser notre objectif global en matière d'analyse de l’impact des événements sociétaux. / Our society has been rapidly growing its presence on the Web, as a consequence we are digitizing a large collection of our daily happenings. In this scenario, the Web receives virtual occurrences of various events corresponding to their real world occurrences from all around the world. Scale of these events can vary from locally relevant ones up to those that receive global attention. News and social media of current times provide all essential means to reach almost a global diffusion. This big data of complex societal events provide a platform to many research opportunities for analyzing and gaining insights into the state of our society.In this thesis, we investigate a variety of social event impact analytics tasks. Specifically, we address three facets in the context of events and the Web, namely, diffusion of events in foreign languages communities, automated classification of Web contents, and news virality assessment and visualization. We hypothesize that the named entities associated with an event or a Web content carry valuable semantic information, which can be exploited to build accurate prediction models. We have shown with the help of multiple studies that raising Web contents to the entity-level captures their core essence, and thus, provides a variety of benefits in achieving better performance in diverse tasks. We report novel findings over disparate tasks in an attempt to fulfill our overall goal on societal event impact analytics.

L'énorme quantité de données dans les réseaux de capteurs vidéo sans fil (WVSN) pour les nœuds de capteurs de ressources limitées augmente les défis liés à la consommation d'énergie et à la consommation de bande passante. La gestion du réseau est l’un des défis de WMSN en raison de l’énorme quantité d’images envoyées simultanément par les capteurs au coordinateur. Dans cette thèse, pour surmonter ces problèmes, plusieurs contributions ont été apportées. Chaque contribution se concentre sur un ou deux défis, comme suit: Dans la première contribution, pour réduire la consommation d'énergie, une nouvelle approche pour l'agrégation des données dans WVSN basée sur des fonctions de similarité des plans est proposée. Il est déployé sur deux niveaux: le niveau du nœud du capteur vidéo et le niveau du coordinateur. Au niveau du nœud de capteur, nous proposons une technique d'adaptation du taux de trame et une fonction de similarité pour réduire le nombre de trames détectées par les nœuds de capteur et envoyées au coordinateur. Au niveau du coordinateur, après avoir reçu des plans de différents nœuds de capteurs voisins, la similarité entre ces plans est calculée pour éliminer les redondances. Dans la deuxième contribution, certains traitements et analyses sont ajoutés en fonction de la similarité entre les images au niveau du capteur-nœud pour n'envoyer que les cadres importants au coordinateur. Les fonctions cinématiques sont définies pour prévoir l'étape suivante de l'intrusion et pour planifier le système de surveillance en conséquence. Dans la troisième contribution, sur la phase de transmission, au niveau capteur-nœud, un nouvel algorithme d'extraction des différences entre deux images est proposé. Cette contribution prend également en compte le défi de sécurité en adaptant un algorithme de chiffrement efficace au niveau du nœud de capteur. Dans la dernière contribution, pour éviter une détection plus lente des intrusions conduisant à des réactions plus lentes du coordinateur, un protocole mac-layer basé sur le protocole S-MAC a été proposé pour contrôler le réseau. Cette solution consiste à ajouter un bit de priorité au protocole S-MAC pour donner la priorité aux données critiques. / The huge amount of data in Wireless Video Sensor Networks (WVSNs) for tiny limited resources sensor nodes increases the energy and bandwidth consumption challenges. Controlling the network is one of the challenges in WMSN due to the huge amount of images sent at the same time from the sensors to the coordinator. In this thesis, to overcome these problems, several contributions have been made. Each contribution concentrates on one or two challenges as follows: In the first contribution, to reduce the energy consumption a new approach for data aggregation in WVSN based on shot similarity functions is proposed. It is deployed on two levels: the video-sensor node level and the coordinator level. At the sensor node level, we propose a frame rate adaptation technique and a similarity function to reduce the number of frames sensed by the sensor nodes and sent to the coordinator. At the coordinator level, after receiving shots from different neighboring sensor nodes, the similarity between these shots is computed to eliminate redundancies. In the second contribution, some processing and analysis are added based on the similarity between frames on the sensor-node level to send only the important frames to the coordinator. Kinematic functions are defined to predict the next step of the intrusion and to schedule the monitoring system accordingly. In the third contribution, on the transmission phase, on the sensor-node level, a new algorithm to extract the differences between two images is proposed. This contribution also takes into account the security challenge by adapting an efficient ciphering algorithm on the sensor node level. In the last contribution, to avoid slower detection of intrusions leading to slower reactions from the coordinator, a mac-layer protocol based on S-MAC protocol has been proposed to control the network. This solution consists in adding a priority bit to the S-MAC protocol to give priority to critical data.

Notre étude se propose de montrer qu'au cours des deux dernières décennies, des années 1989-2009, avec les films de Michael Haneke réalisés pour le cinéma, des innovations décisives apparaissent dans la fiction de nos jours. Des formes nouvelles bouleversent le récit, révélant ce qui, dans la fiction conventionnelle, est devenu stéréotype et mettent en cause la représentation. Des nouveaux rapports entre réel et représentation, entre visible, invisible et insupportable à voir, entre instance énonciative et spectateur entrent en jeu. De nouveaux possibles s'ouvrent sur la voie du développement de la fiction cinématographique et élargissent ses possibilités d'investigation du réel sur l'écran. / Our study suggests that during the last two decades, 1989-2009, with Michael Haneke's movies realized for the cinema, decisive innovations appear in the contemporary fiction. New forms upset the narrative, dispute the representation, and reveal what in the conventional fiction became stereotype. New reports between reality and representation, between visible, invisible and unbearable to see, between the instance of the statement and the spectator come into play. New possibilities open on the way to the development of the film fiction. They widen the possibilities for investigation of the reality on the screen.

Les épilepsies acquises se déclarent après un processus graduel appelé épileptogenèse. Bien que cliniquement silencieux, ce processus implique des modifications fonctionnelles observables notamment par électroencéphalographie. Cette thèse vise i) à identifier des marqueurs électrophysiologiques apparaissant au cours de l’épileptogenèse, et ii) à comprendre les modifications physiopathologiques sous-jacentes responsables de ces marqueurs et de leur évolution temporelle. Dans un premier temps, nous avons, dans un modèle d’épilepsie partielle chez la souris, monitoré des signaux électrophysiologiques intracérébraux pendant la mise en place de la maladie. Nous avons observé dans ces signaux expérimentaux, l’émergence d’événements transitoires pathologiques appelés pointes épileptiques. Nous avons développé des méthodes de traitement du signal pour détecter et caractériser automatiquement ces événements. Ainsi, nous avons pu mettre en évidence certains changements dans la forme des pointes épileptiques au cours de l’épileptogenèse ; en particulier l’apparition et l’augmentation d’une onde qui suit la pointe épileptique. Une hypothèse défendue dans ces travaux est que ces changements morphologiques peuvent constituer des marqueurs de l’épileptogenèse dans ce modèle animal. Dans un second temps, afin d’interpréter ces modifications électrophysiologiques en termes de processus neurophysiologiques sous-jacents, nous avons implémenté un modèle biomathématique, physiologiquement argumenté, capable de simuler des pointes épileptiques. Formellement, ce modèle est un système dynamique non linéaire qui reproduit les interactions synaptiques (excitatrices et inhibitrices) dans une population de neurones. Une analyse de sensibilité de ce modèle a permis de mettre en évidence le rôle critique de certains paramètres de connectivité dans la morphologie des pointes. Nos résultats montrent en effet, qu’une diminution de l’inhibition GABAergique entraîne un accroissement de l’onde dans les pointes épileptiques. À partir du modèle théorique, nous avons pu ainsi émettre des hypothèses sur les modifications opérant au cours du processus d’épileptogenèse. Ces hypothèses ont pu être en partie vérifiées expérimentalement en bloquant artificiellement l’inhibition GABAergique, dans le modèle in vivo chez la souris, et dans un modèle in vitro chez le rat. En conclusion, ce travail de thèse fournit, dans un modèle animal, un biomarqueur électrophysiologique de l’épileptogenèse et tente d’expliquer, grâce à une modélisation biomathématique, les processus neurophysiologiques sous-jacents qu’il reflète. / Acquired epilepsies occur after a process called epileptogenesis. Although clinically silent, this process involves some functional modifications which can be observed by electroencephalography. The objectives of this thesis are i) to identify electrophysiological markers occurring during epileptogenesis, and ii) to understand which underlying pathophysiological modifications are responsible for these markers and their evolution. Firstly, using an in vivo experimental mouse model of partial epilepsy, we have monitored intracranial electrophysiological signals during epileptogenesis. We observed the emergence of pathological transient events called epileptic spikes. We have developed signal processing methods in order to automatically detect and characterize these events. Hence, we observed and quantified morphological changes of epileptic spikes during epileptogenesis. In particular, we noticed the emergence and the increase of a wave which directly follows the spike component. In this work, we defend the hypothesis that these morphological modifications can constitute markers of the epileptogenesis process in this animal model of epilepsy. Secondly, in order to interpret these electrophysiological modifications in terms of underlying pathophysiological processes, we have implemented a computational model able to simulate epileptic spikes. This neural mass model is a neurophysiologically-plausible mesoscopic representation of synaptic interactions (excitation and inhibition) in the hippocampus. Based on a sensitivity analysis of model parameters, we were able to determine some connectivity parameters that play a key role in the morphology of simulated epileptic spikes. In particular, our results show that a diminution of GABAergic inhibition leads to an increase of the aforementioned wave. Thus, using this theoretical model, we defined some hypotheses about pathophysiological modifications occurring during the epileptogenesis process. One of these hypotheses has been confirmed in blocking GABAa receptors in the in vivo mouse model, as well as in an in vitro model (rat, organotypic slices). In summary, based on the shape features of epileptic spikes, we devised an electrophysiological biomarker of epileptogenesis observed in a mouse model but useful in Human studies as well. Moreover, a computational modeling approach has permitted to suggest which pathophysiological processes might underlie this biomarker.

Les signaux électroencéphalographiques enregistrés chez les patients épileptiques reflètent, en dehors des périodes correspondant aux crises d'épilepsie, des signaux transitoires appelés "activités épileptiformes" (AE). L'analyse des AE peut contribuer à l'étude des épilepsies partielles pharmaco-résistantes. Une méthode de caractérisation de la dynamique spatio-temporelle des AE dans des signaux EEG de profondeur est présentée dans ce document. La méthode est constituée de quatre étapes:<br /><br />1. Détection des AE monovoie. La méthode de détection, qui repose sur une approche heuristique, utilise un banc de filtres en ondelettes pour réhausser la composante pointue des AE (généralement appelée "spike" dans la littérature). La valeur moyenne des statistiques obtenues en sortie de chaque filtre est ensuite analysée avec un algorithme de Page-Hinkley dans le but de détecter des changements abrupts correspondant aux spikes.<br /><br />2. Fusion des AE. Cette procédure recherche des co-occurrences entre AE monovoie à l'aide d'une fenêtre glissante puis forme des AE multivoies.<br /><br />3. Extraction des sous-ensembles de voies fréquement et significativement activées lors des AE multivoies (appelés "ensembles d'activation").<br /><br />4. Evaluation de l'éxistence d'un ordre d'activation temporel reproductible (éventuellement partiel) au sein de chaque ensemble d'activation.<br /><br />Les méthodes proposées dans chacune des étapes ont tout d'abord été évaluées à l'aide de signaux simulés (étape 1) ou à l'aide de models Markoviens (étapes 2-4). Les résultats montrent que la méthode complète est robuste aux effets des fausses-alarmes. Cette méthode a ensuite été appliquée à des signaux enregistrés chez 8 patients (chacun contenant plusieurs centaines d'AE). Les résultats indiquent une grande reproductibilité des distributions spatio-temporelles des AE et ont permis l'identification de réseaux anatomo-fonctionnels spécifiques.

Un flot de liens représente une trace de l'activité d'un système complexe au cours du temps, où un lien apparaît lorsque deux entités du système entrent en interaction ; l'ensemble des entités et des liens forme un graphe. Ces traces constituent depuis quelques années des jeux de données stratégiques dans l'analyse de l'activité de systèmes complexes à grande échelle, impliquant des millions d'entités : réseaux de téléphone mobiles, réseaux sociaux, ou encore Internet. Cette thèse porte sur l'analyse exploratoire des flots de liens, en particulier sur la caractérisation de leur dynamique et l'identification d'anomalies au cours du temps (événements). Nous proposons un cadre exploratoire sans hypothèse sur les données, faisant appel à l'analyse statistique et à la visualisation. Les événements détectés sont statistiquement significatifs et nous proposons une méthode pour valider leur pertinence. Nous illustrons enfin notre méthodologie sur l'évolution du réseau social en ligne Github, où des centaines de milliers de développeurs collaborent sur des projets de logiciel.

En raison de la gravité des accidents liés au phénomène de fatigue-propagation de fissure, les préoccupations de l'industrie aéronautique à assurer l'intégrité des structures soumises à ce mode de sollicitation revêtent un caractère tout à fait essentiel. Les travaux de thèse présentés dans ce mémoire visent à appréhender le problème de sûreté des structures aéronautiques dimensionnées en tolérance aux dommages sous l'angle probabiliste. La formulation et l'application d'une approche fiabiliste menant à des processus de conception et de maintenance fiables des structures aéronautiques en contexte industriel nécessitent cependant de lever un nombre important de verrous scientifiques. Les efforts ont été concentrés au niveau de trois domaines dans ce travail. Une méthodologie a tout d'abord été développée afin de capturer et de retranscrire fidèlement l'aléa du chargement de fatigue à partir de séquences de chargement observées sur des structures en service et monitorées, ce qui constitue une réelle avancée scientifique. Un deuxième axe de recherche a porté sur la sélection d'un modèle mécanique apte à prédire l'évolution de fissure sous chargement d'amplitude variable à coût de calcul modéré. Les travaux se sont ainsi appuyés sur le modèle PREFFAS pour lequel des évolutions ont également été proposées afin de lever l'hypothèse restrictive de périodicité de chargement. Enfin, les analyses probabilistes, produits du couplage entre le modèle mécanique et les modélisations stochastiques préalablement établies, ont entre autre permis de conclure que le chargement est un paramètre qui influe notablement sur la dispersion du phénomène de propagation de fissure. Le dernier objectif de ces travaux a ainsi porté sur la formulation et la résolution du problème de fiabilité en tolérance aux dommages à partir des modèles stochastiques retenus pour le chargement, constituant un réel enjeu scientifique. Une méthode de résolution spécifique du problème de fiabilité a été mise en place afin de répondre aux objectifs fixés et appliquée à des structures jugées représentatives de problèmes réels.

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.