Le langage UML est devenu un standard de fait, y compris pour le développement de systèmes critiques. Néanmoins, les outils actuels apportent peu d'aide pour exploiter et vérifier les modèles proposés, surtout en cours de développement. Cette thèse se concentre sur l'aide à la construction d'architectures en UML durant les phases d'analyse et de conception de systèmes réactifs. Elle vise à développer un cadre théorique et pragmatique pour mettre en œuvre une approche incrémentale. Ce cadre fournit un outil permettant de vérifier les architectures durant leur modélisation. Les architectures sont modélisées par des diagrammes UML de structures composites alors que les composants primitifs sont présentés par une combinaison de diagrammes de machines d'états et de diagramme d'activités. Ce travail offre les moyens de vérifier d'une part si une nouvelle architecture est un raffinement, une extension ou un incrément de celle définie durant les étapes précédentes, et d'autre part si un composant est compatible avec un environnement ou s'il est substituable par un autre. L'analyse des architectures impose de leur donner une sémantique formelle. Concernant les composants primitifs, nous leur associons une sémantique en LTS (Labelled Transition Systems) ce qui nous a conduit à définir une procédure de transformation automatique de machines d'états et diagrammes d'activités en LTS. Concernant les composants composites, nous leur associons un LTS en transformant un diagramme de structure composite en une spécification Exp.Open, puis en générant la fusion des LTS grâce à la boîte à outils CADP. Dans un second temps, nous avons mis en œuvre des techniques de vérifications de relations de conformité de LTS que sont les préordres de raffinement, d'extension, et d'incrément. Nous avons également défini et implanté une relation de compatibilité et de substituabilité. L'ensemble de ces techniques de construction incrémentale se positionne selon deux axes. L'axe vertical représente le niveau d'abstraction. L'évolution d'une architecture peut se faire sur cet axe dans deux sens : i) par des techniques de raffinement dans le sens descendant et ii) par des techniques d'abstraction dans le sens ascendant. L'axe horizontal représente le niveau de couverture des exigences. L'évolution d'une architecture peut se faire sur cet axe selon deux sens : i) par des techniques d'extension et ii) par des techniques de restriction. Ces travaux ont été réalisés de façon théorique et pratique : ils ont donné lieu au développement d'un outil dédié à la construction incrémentale de modèles UML, appelé IDCM (Incremental Development of Conforming Models), regroupant la transformation de modèles et la mise en œuvre de l'ensemble des relations incrémentales. Ceci a été validé sur diverses études de cas. / UML is becoming a de facto standard, including for development of dependable systems. However, current tools offer little help to take benefit of proposed models and to verify them, especially during development phases. This thesis focuses on supporting construction of UML architectures of reactive systems. It aims at developing a theoretic and pragmatic framework to implement the incremental approach. The framework provides tools to verify the coherenceof architectures during the modelling phase. Architectures are modelled by UML diagram of composite structures while primitive components are represented by a combination of state machine diagram and activity diagram. This work provides a means to verify in one hand if a new architecture is a refinement, an extension or an increment of those defined in the previous steps, and in another hand, if a component is compatible with an environment or if it is substitutableby another.In order to analyse UML architectures, we must give them a formal semantics. We associated primitive components with LTS (Labelled Transition Systems) which led us to define a procedure for automatic transformation of state machines and activities diagrams into LTS. We associated composite components with LTS by transforming a diagram of composite structure into Exp.Open specification, then by generating LTS fusion with the toolbox CADP. We have implemented verification techniques of conformance relations on LTS such as the preorders: refinement, extension, and increment. We also defined and implemented compatibility relation and substitutability relation. All these incremental construction techniques are positioned along two axes. The vertical axis represents the level of bstraction.The development of an architecture following this axis in two directions: i) refinement techniques in the downward direction and ii) abstraction techniques in the upward direction. The horizontal axis represents the coverage level of requirements. The development of architectures can be realized following this axis in two directions : i) extension direction and ii) restrictiondirection.This work has been carried out in theory and practice : it has led to the development of a dedicated tool for incremental construction of UML models, called IDCM (Incremental Development of Conforming Models), grouping the transformation of models and the implementation of a set of incremental relations. This has been validated on various case studies.

In hyperscale data center operations, automation is applied in many ways as it is becomes very hard to scale otherwise. There are however areas relating to understanding, grouping and diagnosing of error reports that are done manually at Facebook today. This master's thesis investigates solutions for applying unsupervised clustering methods to server error reports, server properties and historical data to speed up and enhance the process of finding and root causing systematic issues. By utilizing data representations that can embed both key-value data and historical event log data, the thesis shows that clustering algorithms together with data representations that capture syntactic and semantic structures in the data can be applied with good results in a real-world scenario.

Two-dimensional scan design is an effective BIST architecture that uses multiple scan chains in parallel to test the Circuit Under Test (CUT). Linear Finite State Machines (LFSMs) are often used as on-board Pseudo Random Pattern Generators (PRPGs) in two-dimensional scan designs. However, linear dependencies present in the LFSM generated test-bit sequences adversely affect the resultant fault coverage in two-dimensional scan designs. In this work, we present methods that improve the resultant fault coverage in two-dimensional scan designs through the minimization of linear dependencies. Currently, metric of channel separation and matrix-based metric are used in order to estimate linear dependencies in a CUT. When the underlying sub-circuit (cone) structure of a CUT is available, the matrix-based metric can be used more effectively. Fisrt, we present two methods that use matrix-based metric and minimize the overall linear dependencies in a CUT through explicitly minimizing linear dependencies in the highest number of underlying cones of the CUT. The first method minimizes linear dependencies in a CUT through the selection of an appropriate LFSM structure. On the other hand, the second method synthesizes a phase shifter for a specified LFSM structure such that the overall linear dependencies in a CUT are minimized. However, the underlying structure of a CUT is not always available and in such cases the metric of channel separation can be used more effectively. The metric of channel separation is an empirical measure of linear dependencies and an ad-hoc large channel separation is imposed between the successive scan chains of a two-dimensional scan design in order to minimize the linear dependencies. Present techniques use LFSMs with additional phase shifters (LFSM/PS) as PRPGs in order to obtain desired levels of channel separation. We demonstrate that Generalized LFSRs (GLFSRs) are a better choice as PRPGs compared to LFSM/PS and obtain desired levels of channel separations at a lower hardware cost than the LFSM/PS. Experimental results corroborate the effectiveness of the proposed methods through increased levels of the resultant fault coverage in two-dimensional scan designs.

The traffic signal affects the life of virtually everyone every day. The effectiveness of signal systems can reduce the incidence of delays, stops, fuel consumption, emission of pollutants, and accidents. The problems related to rapid growth in traffic congestion call for more effective traffic signalization using robust feedback control methodology. Online traffic-responsive signalization is based on real-time traffic conditions and selects cycle, split, phase, and offset for the intersection according to detector data. A robust traffic feedback control begins with assembling traffic demands, traffic facility supply, and feedback control law for the existing traffic operating environment. This information serves the input to the traffic control process which in turn provides an output in terms of the desired performance under varying conditions. Traffic signalization belongs to a class of hybrid systems since the differential equations model the continuous behavior of the traffic flow dynamics and finite-state machines model the discrete state changes of the controller. A complicating aspect, due to the state-space constraint that queue lengths are necessarily nonnegative, is that the continuous-time system dynamics is actually the projection of a smooth system of ordinary differential equations. This also leads to discontinuities in the boundary dynamics of a sort common in queueing problems. The project is concerned with the design of a feedback controller to minimize accumulated queue lengths in the presence of unknown inflow disturbances at an isolated intersection and a traffic network with some signalized intersections. A dynamical system has finite L₂-gain if it is dissipative in some sense. Therefore, the H<SUB>infinity</SUB>-control problem turns to designing a controller such that the resulting closed loop system is dissipative, and correspondingly there exists a storage function. The major contributions of this thesis include 1) to propose state space models for both isolated multi-phase intersections and a class of queueing networks; 2) to formulate H<SUB>infinity</SUB> problems for the control systems with persistent disturbances; 3) to present the projection dynamics aspects of the problem to account for the constraints on the state variables; 4) formally to study this problem as a hybrid system; 5) to derive traffic-actuated feedback control laws for the multi-phase intersections. Though we have mathematically presented a robust feedback solution for the traffic signalization, there still remains some distance before the physical implementation. A robust adaptive control is an interesting research area for the future traffic signalization. / Ph. D.

Spectrum sensing in wireless communications serves as a crucial binary classification tool in cognitive radios, facilitating the detection of available radio spectrums for secondary users, especially in scenarios with high Signal-to-Noise Ratio (SNR). Leveraging Liquid State Machines (LSMs), which emulate spiking neural networks like the ones in the human brain, prove to be highly effective for real-time data monitoring for such temporal tasks. The inherent advantages of LSM-based recurrent neural networks, such as low complexity, high power efficiency, and accuracy, surpass those of traditional deep learning and conventional spectrum sensing methods. The architecture of the liquid state machine processor and its training methods are crucial for the performance of an LSM accelerator. This thesis presents one such LSM-based accelerator that explores novel architectural improvements for LSM hardware. Through the adoption of triplet-based Spike-Timing-Dependent Plasticity (STDP) and various spike encoding schemes on the spectrum dataset within the LSM, we investigate the advantages offered by these proposed techniques compared to traditional LSM models on the FPGA. FPGA boards, known for their power efficiency and low latency, are well-suited for time-critical machine learning applications. The thesis explores these novel onboard learning methods, shares the results of the suggested architectural changes, explains the trade-offs involved, and explores how the improved LSM model's accuracy can benefit different classification tasks. Additionally, we outline the future research directions aimed at further enhancing the accuracy of these models. / Master of Science / Machine Learning (ML) and Artificial Intelligence (AI) have significantly shaped various applications in recent years. One notable domain experiencing substantial positive impact is spectrum sensing within wireless communications, particularly in cognitive radios. In light of spectrum scarcity and the underutilization of RF spectrums, accurately classifying spectrums as occupied or unoccupied becomes crucial for enabling secondary users to efficiently utilize available resources. Liquid State Machines (LSMs), made of spiking neural networks resembling human brain, prove effective in real-time data monitoring for this classification task. Exploiting the temporal operations, LSM accelerators and processors, facilitate high performance and accurate spectrum monitoring than conventional spectrum sensing methods. The architecture of the liquid state machine processor's training and optimal learning methods plays a pivotal role in the performance of a LSM accelerator. This thesis delves into various architectural enhancements aimed at spectrum classification using a liquid state machine accelerator, particularly implemented on an FPGA board. FPGA boards, known for their power efficiency and low latency, are well-suited for time-critical machine learning applications. The thesis explores onboard learning methods, such as employing a targeted encoder and incorporating Triplet Spike Timing-Dependent Plasticity (Triplet STDP) in the learning reservoir. These enhancements propose improvements in accuracy for conventional LSM models. The discussion concludes by presenting results of the architectural implementations, highlighting trade-offs, and shedding light on avenues for enhancing the accuracy of conventional liquid state machine-based models further.

<p>This Ph.D. thesis addresses topics related to overlay networks, their de_nition,<br />formalization and applications. Descriptions of the Chord and Synapse protocols using<br />the ASM formalism is presented, and both a high-level and a re_ned proof of the<br />correctness of the Chord formalization is given. A probabilistic assessment of the<br />exhaustiveness of the Synapse protocol is performed. An updated version of the<br />Proposal of metadata schemata for movable cultural heritage as well as a Proposal of<br />metadata schemata for describing collections are provided. Based of the Chord protocol, a Distributed catalog of digitized collections of Serbian cultural herigate is implemented.</p> / <p>Doktorska disertacija se bavi temama vezanim za prekrivajuće mreže, njihovom<br />definicijom, formalizacijom i primenama. Dati su opisi Chord i Synapse protokola<br />kori&scaron;ćenjem ASM formalizma, kao i dokaz korektnosti formalizacije Chord protokola<br />na visokom nivou, kao i njegovo profinjenje. Izvr&scaron;ena je verovatnosna ocena uspe&scaron;nosti pretrage pomoću Synapse protokola. Predstavljena je ažurirana verzija Predloga sheme meta podataka za pokretna kulturna dobra, kao i Predlog sheme meta podataka za opis kolekcija. Implementiran je Distribuirani katalog digitalizovanih kolekcija kulturne ba&scaron;tine Srbije zasnovan na Chord protokolu.</p>

O objetivo deste trabalho é tornar possível a inserção de um robô humanoide para auxiliar pacientes em sessões de fisioterapia. Um sistema robótico é proposto que utiliza um robô humanoide, denominado NAO, visando analisar os movimentos feitos pelos pacientes e corrigi-los se necessário, além de motivá-los durante uma sessão de fisioterapia. O sistema desenvolvido permite que o robô, em primeiro lugar, aprenda um exercício correto de fisioterapia observando sua execução por um fisioterapeuta; em segundo lugar, que ele demonstre o exercício para que um paciente possa imitá-lo; e, finalmente, corrija erros cometidos pelo paciente durante a execução do exercício. O exercício correto é capturado por um sensor Kinect e dividido em uma sequência de estados em dimensão espaço-temporal usando k-means clustering. Estes estados então formam uma máquina de estados finitos para verificar se os movimentos do paciente estão corretos. A transição de um estado para o próximo corresponde a movimentos parciais que compõem o movimento aprendido, e acontece somente quando o robô observa o mesmo movimento parcial executado corretamente pelo paciente; caso contrário o robô sugere uma correção e pede que o paciente tente novamente. O sistema foi testado com vários pacientes em tratamento fisioterapêutico para problemas motores. Os resultados obtidos, em termos de precisão e recuperação para cada movimento, mostraram-se muito promissores. Além disso, o estado emocional dos pacientes foi também avaliado por meio de um questionário aplicado antes e depois do tratamento e durante o tratamento com um software de reconhecimento facial de emoções e os resultados indicam um impacto emocional bastante positivo e que pode vir a auxiliar pacientes durante tratamento fisioterapêuticos. / This dissertation develops a robotic system to guide patients through physiotherapy sessions. The proposed system uses the humanoid robot NAO, and it analyses patients movements to guide, correct, and motivate them during a session. Firstly, the system learns a correct physiotherapy exercise by observing a physiotherapist perform it; secondly, it demonstrates the exercise so that the patient can reproduce it; and finally, it corrects any mistakes that the patient might make during the exercise. The correct exercise is captured via Kinect sensor and divided into a sequence of states in spatial-temporal dimension using k-means clustering. Those states compose a finite state machine that is used to verify whether the patients movements are correct. The transition from one state to the next corresponds to partial movements that compose the learned exercise. If the patient executes the partial movement incorrectly, the system suggests a correction and returns to the same state, asking that the patient try again. The system was tested with multiple patients undergoing physiotherapeutic treatment for motor impairments. Based on the results obtained, the system achieved high precision and recall across all partial movements. The emotional impact of treatment on patients was also measured, via before and after questionnaires and via a software that recognizes emotions from video taken during treatment, showing a positive impact that could help motivate physiotherapy patients, improving their motivation and recovery.

A realização de atividades de teste é indispensável para a garantia da qualidade de um produto e para a identificação de defeitos, diminuindo custos de manutenção e evitando ao máximo o risco do cliente encontrar esses defeitos. Nessa linha, testes baseados em modelos têm se mostrado atrativos, pois o custo de geração de casos de testes e de correção de defeitos tende a ser menor. Devido à sua simplicidade conceitual e expressividade na descrição do comportamento de um sistema, um dos modelos mais usados e pesquisados na área de teste baseado em modelos são as Máquinas de Estados Finitos (MEFs). Por meio de MEFs e com apoio de ferramentas apropriadas, a geração de casos de testes para avaliar os comportamentos esperados de um sistema é automatizada, reduzindo tanto o custo da geração e da manutenção quanto as falhas humanas. Desta forma, a aplicabilidade de métodos de geração de casos de teste baseados em modelos no contexto de sistemas embarcados vem sendo investigada. O objetivo deste trabalho de mestrado consiste em investigar a aplicabilidade dos métodos de geração em cenários de teste reais, com foco em sistemas embarcados, identificando as difi- culdades e limitações do processo, bem como os requisitos essenciais para a adequação dos métodos de geração propostos na literatura e de ferramentas de apoio à atividade de teste. O foco principal do projeto é a implementação de mecanismos que atendam aos requisitos levantados, visando a usabilidade, segurança e portabilidade da ferramenta / Test activities are essential to ensure the quality of products and identify faults to reduce maintenance costs and avoid that the client finds these faults. In this sense, model-based tests have been proved useful, because the cost of generating test cases and fault correction tend to be smaller. Due to its conceptual simplicity and expressiveness in describing the behavior of a system, Finite State Machines (FSM) have been used and researched in the model-based testing area. FSMs, employed with the support of appropriate tools, enable the generation of test cases in an automated way to assess the expected behavior of a system, reducing both the generation and maintenance costs and human failures. Thus, the applicability of test cases generation methods based on models in the context of embedded systems should be investigated. Test cases generation methods based on FSM are designed to derive test cases from the model. In this context, this work aims to investigate the applicability of generation methods in real-world scenarios, focusing embedded systems. It should identify the difficulties and limitations of the process, as well as the essential requirements for the adequacy of generation methods proposed in the literature and tools to support the test activity. The main focus of the project is the implementation of mechanisms that meet the elicited requirements in order to provide usability, security and tool portability

A ideia de usar redes neurais biologicamente inspiradas na computação tem sido amplamente utilizada nas últimas décadas. O fato essencial neste paradigma é que um neurônio pode integrar e processar informações, e esta informação pode ser revelada por sua atividade de pulsos. Ao descrever a dinâmica de um único neurônio usando um modelo matemático, uma rede pode ser implementada utilizando um conjunto desses neurônios, onde a atividade pulsante de cada neurônio irá conter contribuições, ou informações, da atividade pulsante da rede em que está inserido. Neste trabalho é apresentado um controlador de posição no eixo Z utilizando fusão de sensores baseado no paradigma de Redes Neurais Recorrentes. O sistema proposto utiliza uma Máquina de Estado Líquido (LSM) para controlar o robô colaborativo BAXTER. O framework foi projetado para trabalhar em paralelo com as LSMs que executam trajetórias em formas fechadas de duas dimensões, com o objetivo de manter uma caneta de feltro em contato com a superfície de desenho, dados de sensores de força e distância são alimentados ao controlador. O sistema foi treinado utilizando dados de um controlador Proporcional Integral Derivativo (PID), fundindo dados de ambos sensores. Resultados mostram que a LSM foi capaz de aprender o comportamento do controlador PID em diferentes situações. / The idea of employing biologically inspired neural networks to perform computation has been widely used over the last decades. The essential fact in this paradigm is that a neuron can integrate and process information, and this information can be revealed by its spiking activity. By describing the dynamics of a single neuron using a mathematical model, a network in which the spiking activity of every single neuron will get contributions, or information, from the spiking activity of the embedded network. A positioning controller based on Spiking Neural Networks for sensor fusion suitable to run on a neuromorphic computer is presented in this work. The proposed framework uses the paradigm of reservoir computing to control the collaborative robot BAXTER. The system was designed to work in parallel with Liquid State Machines that performs trajectories in 2D closed shapes. In order to keep a felt pen touching a drawing surface, data from sensors of force and distance are fed to the controller. The system was trained using data from a Proportional Integral Derivative controller, merging the data from both sensors. The results show that the LSM can learn the behavior of a PID controller on di erent situations.

Os sistemas produtivos (SPs) podem utilizar controladores programáveis (CPs) como dispositivos de realização do controle. Neste contexto, programas de controle executados por estes CPs podem ser desenvolvidos de forma que não estejam em conformidade com as especificações de projeto, o que poderá provocar o surgimento de erros funcionais associados à execução de tais programas de controle, erros estes que podem levar os SPs sob controle a um estado que poderá implicar em acidentes envolvendo equipamentos, pessoas e o meio-ambiente. Esta questão tem motivado o surgimento de diversas abordagens para identificar a existência de erros em programas de controle de CPs, de forma a permitir a correção destes erros e garantir, conseqüentemente, maior confiabilidade operacional. O presente trabalho tem por objetivo identificar a existência de erros em programas de controle baseados em LD (Ladder Diagram). Para isto, propõe-se um procedimento de desenvolvimento de modelos baseados em máquinas de estados finitos estendidas (MEFEs), que são gerados a partir do mapeamento de cada um dos rungs contidos no programa de controle que se deseja identificar erros. Uma vez desenvolvidos os modelos em MEFEs, torna-se possível a utilização de uma ferramenta computacional de verificação, própria para estabelecer se os modelos verificados satisfazem determinadas proposições estabelecidas em lógica temporal. Uma proposição em lógica temporal está relacionada a um estado específico do programa de controle modelado, sendo que o objetivo da verificação é o de estabelecer se a proposição estipulada é atendida ou não. Se um determinado estado específico for, por exemplo, um estado indesejado do programa de controle modelado, e este estado for possível de ser alcançado como resultado do processo de verificação realizado, isto impactará na não conformidade do programa de controle com as especificações comportamentais estipuladas na forma de proposição em lógica temporal, indicando haver, portanto, um erro neste programa de controle modelado. Palavras-chave: Controladores programáveis. Linguagem de programação LD. Modelagem e verificação de máquinas de estados finitos estendidas (MEFEs). / Productive systems (PS) can use programmable logic controllers (PLCs) as the devices of accomplishment of the control. In this context, control programs executed by these PLCs can be developed in a way so that they can be in non-conformity with the project specifications, and this fact may result in functional errors related to the control programs execution. These errors can take the PS under control to a state which can lead into accidents involving equipment, people and the environment. This fact has motivated the appearance of different approaches so as to identify the existence of these errors in PLC control programs so that they can be corrected and assure a greater operational reliability. This work aims at identifying the existence of errors in control programs based on Ladder Diagram (LD). In order to accomplish that, a modeling procedure that generates extended finite state machines (EFSMs) is proposed from the mapping of each one of the rungs in the control program whose errors are to be identified. Once the models based on EFSMs are developed it becomes possible to use a computational verification tool, specifically designed to determine if the verified models fulfill determined propositions established in temporal logic. A proposition in temporal logic is related to a specific state of the modeled control program and the objective of the verification is to establish whether the proposition is fulfilled or not. If a determined specific state, for example, is an unwanted state of the modeled control program and if this state is reachable as a result of the verification process, this will impact in the non-conformity of the control program with the behavior specifications established in a temporal logic proposition, indicating an error in this modeled control program.