Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du π-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le π-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le π-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du π-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles. / We are interested in analyzing the performability requirements of mobile communication systems by using model checking techniques. We model these systems using a high-level formalism derived from the π-calculus, for considering stochastic, timed, deterministic or indeterministic behaviors. However, in the π-calculus, the basic communication primitive of systems is the synchronous point-to-point communication. However, mobile systems that use wireless networks, mostly communicate by local broadcast. Therefore, we first define the broadcast communication into the π-calculus, to better model the systems we study. We propose to use probabilistic and stochastic versions of the algebra we have defined to allow performance studies. We define a temporal version to consider time in the models. But the lack of tools for analyzing properties of models specified with π-calculus is a major obstacle to our work and its objectives. The definition of translation rules into the PRISM language allows us to translate our models in low-level models which can support model checking, namely discrete time, or continuous time Markov chains, timed automata, or probabilistic timed automata. We chose the PRISM model checker because, in our best knowledge, in its latest version, it is the only tool that supports the low-level formalisms that we have previously cited, and thus, makes it possible to realize complete performability studies. This approach allows us to overcome the lack of model checkers for our models. Subsequently, we apply these theoretical concepts to analyse performability of mobile wireless sensor networks.

No description available.

Syfte och frågeställningar Syftet med den här studien har varit att undersöka och jämföra kvinnor och män i åldersgrupperna 30-39 år respektive 40-49 år avseende antropometriska mått samt prestation på GIH:s hälsotester. En vidare målsättning var att undersöka om det förekom några skillnader mellan två separata testtillfällen. Frågeställningarna har varit om resultaten på hälsotesterna skiljer sig mellan könen, åldersgrupperna samt mellan två separata testtillfällen. Metod Totalt fullföljde 41 deltagare GIH:s hälsotester, av dem var 20 kvinnor och 21 män mellan 30-49 år. Det enda som krävdes för att delta var att man uppfattade sig själv som frisk. Personer som tidigare haft stroke, hjärtinfarkt eller opererats på grund av hjärtproblem har inte inkluderats, ej heller gravida och personer med ledbesvär. Testerna utfördes på LTIV (Laboratoriet för tillämpad idrottsvetenskap) mellan februari och mars 2016. Resultat Signifikanta skillnader mellan de två separata testtillfällena noterades för några av styrketesterna framför allt hos männen: axelpressar, handgrip och stolresningar. Mellan könen sågs signifikanta skillnader i de antropometriska måtten, samt i flera konditions- och styrketester. Bland dessa kunde signifikant högre värden ses för kvinnorna än för männen i ryggstyrketestet.  Signifikanta skillnader mellan åldersgrupperna 30-39 år och 40-49 år sågs näst intill endast för kvinnor. De yngre jämfört med de äldre kvinnorna presterade bättre i flera av testerna, de vägde mindre och hade mindre kroppsmått. Slutsats Det framkom vanligtvis inte några signifikanta skillnader mellan det första och andra testtillfället, med enstaka undantag. När så är fallet behövs bara ett test utföras initialt inför en period med exempelvis fysisk aktivitet som senare kanske ska följas upp med ett återtest. Skillnader mellan könen och olika åldersgrupper framkom i vissa tester men inte i alla. Resultaten i denna studie beror bland annat på urvalet av individer. Eftersom att syftet med den här studien har varit att endast utföra de tester som ingår i GIH:s hälsotester har inga tester lagts till eller exkluderats. I arbetet diskuteras bland annat hur optimala testerna är som ett mått på hälsa. För att effektivisera hälsotestundersökningar framöver behöver nödvändigtvis inte alla tester utföras.

Turn-taking is a fundamental process that governs social interaction. When humans interact, they naturally take initiative and relinquish control to each other using verbal and nonverbal behavior in a coordinated manner. In contrast, existing approaches for controlling a robot's social behavior do not explicitly model turn-taking, resulting in interaction breakdowns that confuse or frustrate the human and detract from the dyad's cooperative goals. They also lack generality, relying on scripted behavior control that must be designed for each new domain. This thesis seeks to enable robots to cooperate fluently with humans by automatically controlling the timing of multimodal turn-taking. Based on our empirical studies of interaction phenomena, we develop a computational turn-taking model that accounts for multimodal information flow and resource usage in interaction. This model is implemented within a novel behavior generation architecture called CADENCE, the Control Architecture for the Dynamics of Embodied Natural Coordination and Engagement, that controls a robot's speech, gesture, gaze, and manipulation. CADENCE controls turn-taking using a timed Petri net (TPN) representation that integrates resource exchange, interruptible modality execution, and modeling of the human user. We demonstrate progressive developments of CADENCE through multiple domains of autonomous interaction encompassing situated dialogue and collaborative manipulation. We also iteratively evaluate improvements in the system using quantitative metrics of task success, fluency, and balance of control.

Ce travail est consacré à la problématique du suivi des systèmes répartis temps réel. Plus précisément, il se concentre sur les aspects formels de la supervision basée sur des modèles ainsi que sur les problèmes qui lui sont liés. Dans la première partie du travail, nous présentons les propriétés de base de deux modèles formels bien connus utilisés pour la modélisation de systèmes répartis : les réseaux d'automates temporisés et les réseaux de Petri temporels. Nous montrons que le comportement de ces modèles peut être représenté par les procédés dits de branchement. Nous introduisons également les éléments conceptuels clés du système de surveillance. La deuxième partie du travail est consacrée à la question des dépliages avec contraintes qui permettent le suivi des relations causales entre les événements dans un système réparti. Ce type de structure peut reproduire des processus sur la base d'un ensemble totalement non-ordonné d'évènements. Dans notre travail, nous soulevons les problèmes des contraintes de temps et de leurs paramétrages. Les méthodes proposées sont illustrées par des études de cas. La troisième partie du travail traite de la problématique des boucles inobservables qui peuvent résulter de comportements cycliques inobservables des systèmes considérés. Ce type de comportement conduit à un nombre infini d'événements dans les dépliages avec contraintes. La quatrième et dernière partie du travail est consacrée à l'implémentation des méthodes décrites précédemment. / This work is devoted to the issue of monitoring of distributed real-time systems. In particular, it focuses on formal aspects of model-based supervision and problems which are related to it. In its first part, we present the basic properties of two well-known formal models used to model distributed systems: networks of timed automata and time Petri nets. We show that the behavior of these models can be represented with so-called branching processes. We also introduce the key conceptual elements of the supervisory system. The second part of the work is dedicated to the issue of constrained unfoldings which enable us to track causal relationships between events in a distributed system. This type of structure can be used to reproduce processes of the system on the basis of a completely unordered set of previously observed events. Moreover, we show that time constraints imposed on a system and observations submitted to the supervisory system can significantly affect a course of events in the system. We also raise the issue of parameters in time constraints. The proposed methods are illustrated with case studies. The third part of the work deals with the issue of unobservable cyclical behaviors in distributed systems. This type of behaviors leads to an infinite number of events in constrained unfoldings. We explain how we can obtain a finite structure that stores information about all observed events in the system, even if this involves processes that are infinite due to such unobservable loops. The fourth and final part of the work is dedicated to implementation issues of the previously described methods.

Submitted by Natalia de Souza Gonçalves (natalia.goncalves@ufpe.br) on 2016-09-28T12:33:15Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) GustavoHPCarvalho_Doutorado_CInUFPE_2016.pdf: 1763137 bytes, checksum: aed7b3ab2f6235757818003678633c9b (MD5) / Made available in DSpace on 2016-09-28T12:33:15Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) GustavoHPCarvalho_Doutorado_CInUFPE_2016.pdf: 1763137 bytes, checksum: aed7b3ab2f6235757818003678633c9b (MD5) Previous issue date: 2016-02-26 / High trustworthiness levels are usually required when developing critical systems, and model based testing (MBT) techniques play an important role generating test cases from specification models. Concerning critical systems, these models are usually created using formal or semi-formal notations. Moreover, it is also desired to clearly and formally state the conditions necessary to guarantee that an implementation is correct with respect to its specification by means of a conformance relation, which can be used to prove that the test generation strategy is sound. Despite the benefits of MBT, those who are not familiar with the models syntax and semantics may be reluctant to adopt these formalisms. Furthermore, most of these models are not available in the very beginning of the project, when usually natural-language requirements are available. Therefore, the use of MBT is postponed. Here, we propose an MBT strategy for generating test cases from controlled naturallanguage (CNL) requirements: NAT2TEST, which refrains the user from knowing the syntax and semantics of the underlying notations, besides allowing early use of MBT via naturallanguage processing techniques; the formal and semi-formal models internally used by our strategy are automatically generated from the natural-language requirements. Our approach is tailored to data-flow reactive systems: a class of embedded systems whose inputs and outputs are always available as signals. These systems can also have timed-based behaviour, which may be discrete or continuous. The NAT2TEST strategy comprises a number of phases. Initially, the requirements are syntactically analysed according to a CNL we proposed to describe data-flow reactive systems. Then, the requirements informal semantics are characterised based on the case grammar theory. Afterwards, we derive a formal representation of the requirements considering a model of dataflow reactive systems we defined. Finally, this formal model is translated into communicating sequential processes (CSP) to provide means for generating test cases. We prove that our test generation strategy is sound with respect to our timed input-output conformance relation based on CSP: csptio. Besides CSP, we explore the generation of other target notations (SCR and IMR) from which we can generate test cases using commercial tools (T-VEC and RT-Tester, respectively). The whole process is fully automated by the NAT2TEST tool. Our strategy was evaluated considering examples from the literature, the aerospace (Embraer) and the automotive (Mercedes) industry. We analysed performance and the ability to detect defects generated via mutation. In general, our strategy outperformed the considered baseline: random testing. We also compared our strategy with relevant commercial tools. / Testes baseados em modelos (MBT) consiste em criar modelos para especificar o comportamento esperado de sistemas e, a partir destes, gerar testes que verificam se implementações possuem o nível de confiabilidade esperado. No contexto de sistemas críticos, estes modelos são normalmente (semi)formais e deseja-se uma definição precisa das condições necessárias para garantir que uma implementação é correta em relação ao modelo da especificação. Esta definição caracteriza uma relação de conformidade, que pode ser usada para provar que uma estratégia de MBT é consistente (sound). Apesar dos benefícios, aqueles sem familiaridade com a sintaxe e a semântica dos modelos empregados podem relutar em adotar estes formalismos. Aqui, propõe-se uma estratégia de MBT para gerar casos de teste a partir de linguagem natural controlada (CNL). Esta estratégia (NAT2TEST) dispensa a necessidade de conhecer a sintaxe e a semântica das notações formais utilizadas internamente, uma vez que os modelos intermediários são gerados automaticamente a partir de requisitos em linguagem natural. Esta estratégia é apropriada para sistemas reativos baseados em fluxos de dados: uma classe de sistemas embarcados cujas entradas e saídas estão sempre disponíveis como sinais. Estes sistemas também podem ter comportamento dependente do tempo (discreto ou contínuo). Na estratégia NAT2TEST, inicialmente, os requisitos são analisados sintaticamente de acordo com a CNL proposta neste trabalho para descrever sistemas reativos. Em seguida, a semântica informal dos requisitos é caracterizada utilizando a teoria de gramática de casos. Posteriormente, deriva-se uma representação formal dos requisitos considerando um modelo definido neste trabalho para sistemas reativos. Finalmente, este modelo é traduzido em uma especificação em communicating sequential processes (CSP) para permitir a geração de testes. Este trabalho prova que a estratégia de testes proposta é consistente considerando a relação de conformidade temporal baseada em entradas e saídas também definida aqui: csptio. Além de CSP, foi explorada a geração de outras notações formais (SCR e IMR), a partir das quais é possível gerar casos de teste usando ferramentas comerciais (T-VEC e RT-Tester, respectivamente). Todo o processo é automatizado pela ferramenta NAT2TEST. A estratégia NAT2TEST foi avaliada considerando exemplos da literatura, da indústria aeroespacial (Embraer) e da automotiva (Mercedes). Foram analisados o desempenho e a capacidade de detectar defeitos gerados através de operadores de mutação. Em geral, a estratégia NAT2TEST apresentou melhores resultados do que a referência adotada: testes aleatórios. A estratégia NAT2TEST também foi comparada com ferramentas comerciais relevantes.

Les vibrations du sol induites par les activités humaines telles que, les activités industrielles, la circulation des camions et voitures, les explosions dues aux constructions ou l’exploitation de la déconstruction, atteignent souvent la limite de gêne pour les usagers et parfois la limite de nocivité. Dans les régions urbaines à forte densité et pour les bâtiments abritant des équipements sensibles, les vibrations du sol doivent être strictement contrôlées. Jusqu'à présent, de nombreuses méthodes de réduction de vibration ont été proposées, dont l'une est l'installation d'une barrière d'ondes entre les sources et les structures à protéger. Au cours des dernières décennies, l'efficacité de l'isolation des vibrations à l’aide de barrière d'ondes a été étudiée. Toutefois, il y a peu de travaux consacrés à l’influence mutuelle des paramètres du système sol-barrière sur l'efficacité de l'isolation de la barrière d'ondes, et l'optimisation de la barrière d'onde est également rare. D'autre part, l'influence des vibrations du sol, générées par les explosions durant la construction d’un nouveau tunnel, sur un tunnel avoisinant, interpelle en raison des dommages qui peuvent être produits. Jusqu'à présent, il existe peu de mesures d'atténuation globale proposées par les chercheurs et les ingénieurs concernant la réduction de vibrations dans les tunnels lors des explosions. Pour répondre à ces insuffisances, cette thèse porte sur l'étude de l'influence des différents paramètres du système sol-barrière et qualifie l'efficacité de l'isolation de la barrière d'ondes. Les paramètres clés sont identifiés, leur rôle respectif quantifié. Plus important encore, une méthode de conception d'optimisation est mise au point, dans le but de proposer la barrière qui est capable de réduire au minimum la vibration du sol en site protégé. Enfin, le comportement dynamique du tunnel existant sous les sollicitations des explosions proches est examiné. Les paramètres qui influent considérablement sur la réponse du tunnel sont mis en évidence. Deux mesures d'atténuation pratiques, concernant l'installation d'une couche de protection le long de la paroi du tunnel d’une part et des explosions à retardement (plutôt que des explosions instantanées) d’autre part, sont présentées en détails. Les recherches menées dans le cadre de cette thèse sont en mesure de fournir des éléments pour la conception optimisée de la barrière d'ondes afin de réduire les vibrations du sol en site protégé et pour la conception de mesures d'atténuation concrètes afin de protéger un tunnel existant par des explosions à proximité. / Ground vibration induced by human activity such as industrial activities, car or truck traffic, or pilling and blasting in construction or deconstruction operation, generally reaches the troublesome limit for men and occasionally attains the harmful limit. In the densely populated urban regions and buildings housing sensitive equipments, ground vibration has to be strictly controlled. Up to now, many vibration reduction methods have been proposed, one of which is the installation of wave barrier between the dynamic sources and the protected structures. Over the past decades, the vibration isolation effectiveness of wave barrier has been extensively studied. However, to the best of the writer’s knowledge, there is little study about the mutual influence of the parameters of soil-barrier system on the barrier screening efficiency, and the optimization design for wave barrier is rare as well. On the other hand, the influence of ground vibration generated by explosions on the nearby existing tunnel has attracted more and more attention due to the recent damage or even failure of tunnels. Up to now, there are few mitigation measures comprehensively proposed by researchers and engineers for the tunnel vibration reduction during explosions. To overcome those drawbacks, this dissertation focuses on the investigation of the influence of various parameters of soil-barrier system on the barrier isolation efficiency. Key parameters are identified. More importantly, an optimization design method is developed, aiming to find out the desirable barrier that is able to minimize the ground vibration in protected site. Besides, the dynamic behavior of existing tunnel under nearby explosions is examined. Parameters that significantly affect the response of tunnel are pointed out. Furthermore, two practical mitigation measures: the installation of a protective layer along the tunnel lining and time-delayed explosions (rather than instantaneous explosions), are presented with details. The research in this dissertation is able to provide a good reference for the optimization design of wave barrier in reducing ground vibration in protected site and for the design of practical mitigation measures to protect existing tunnel from nearby explosions.

<p align="justify">Computer Science is currently facing a grand challenge :finding good design practices for embedded systems. Embedded systems are essentially computers interacting with some physical process. You could find one in a braking systems or in a nuclear power plant for example. They present several design difficulties :first they are reactive systems, interacting indefinitely with their environment. Second,they must satisfy real-time constraints specifying when they should respond, and not only how. Finally, their environment is often deeply continuous, presenting complex dynamics. The formal models of choice for specifying such systems are timed and hybrid automata for which model checking is pretty well studied.</p> <p><p align="justify">In a first part of this thesis, we study a complete design approach, including verification and code generation, for timed automata. We have to define a new semantics for timed automata, the AASAP semantics, that preserves the decidability properties for model checking and at the same time is implementable. Our notion of implementability is completely novel, and relies on the simulation of a semantics that is obviously implementable on a real platform. We wrote tools for the analysis and code generation and exemplify them on a case study about the well known Philips Audio Control Protocol.</p> <p><p align="justify">In a second part of this thesis, we study the problem of controller synthesis for an environment specified as a hybrid automaton. We give a new solution for discrete controllers having only an imperfect information about the state of the system. In the process, we defined a new algorithm, based on the monotonicity of the controllable predecessors operator, for efficiently finding a controller and we show some promising applications on a classical problem :the universality test for finite automata. / Doctorat en sciences, Spécialisation Informatique / info:eu-repo/semantics/nonPublished

Tato práce se zabývá problematikou popisu síťového provozu pomocí automaticky vytvořeného modelu komunikace. Hlavním zaměřením jsou komunikace v řídicích systémech , které využívají speciální protokoly, jako je například IEC 60870-5-104 . V této práci představujeme metodu charakteristiky síťového provozu z pohledu obsahu komunikace i chování v čase. Tato metoda k popisu využívá deterministické konečné automaty , prefixové stromy  a analýzu opakovatelnosti. Ve druhé části této diplomové práce se zaměřujeme na implementaci programu, který je schopný na základě takového modelu komunikace verifikovat síťový provoz v reálném čase.

This project deals with given safeguard possibilities, both mechanical and electronic. A row house with garden was chosen for being secured. Subsequently, were elaborated two`s proposals of securing and guarding of this object. First, was based on camera`s system and second on common system ESS. Later on they were evaluated and the most considerable benefits were emphasized. A system based on control panel with connected detectors was selected upon specification. Subsequently was created a model of the chosen system, at which the required behaviour was simulated and verified. An outline of an implementation was created in the C language.