The complexity of the software behind autonomous systems is rapidly growing, as are the applications of what they can do. It is not unusual for the lines of code to reach the millions, which adds to the verification challenge. The machine learning algorithms involved are often "black boxes" where the precise workings are not known by the developer applying them, and their behavior is undefined when encountering an untrained scenario. With so much code, the possibility of bugs or malicious code is considerable. An approach is developed to monitor and possibly override the behavior of autonomous systems independent of the software controlling them. Application-isolated safety monitors are implemented in configurable hardware to ensure that the behavior of an autonomous system is limited to what is intended. The sensor inputs may be shared with the software, but the output from the monitors is only engaged when the system violates its prescribed behavior. For each specific rule the system is expected to follow, a monitor is present processing the relevant sensor information. The behavior is defined in linear temporal logic (LTL) and the associated monitors are implemented in a field programmable gate array (FPGA). An off-the-shelf drone is used to demonstrate the effectiveness of the monitors without any physical modifications to the drone. Upon detection of a violation, appropriate corrective actions are persistently enforced on the autonomous system. / Master of Science / Autonomous systems are surprisingly vulnerable, not just from malicious hackers, but from design errors and oversights. The lines of code required can quickly climb into the millions, and the artificial decision algorithms can be inscrutable and fully dependent upon the information they are trained on. These factors cause the verification of the core software running our autonomous cars, drones, and everything else to be prohibitively difficult by traditional means. Independent safety monitors are implemented to provide internal oversight for these autonomous systems. A semi-automatic design process efficiently creates error-free monitors from safety rules drones need to follow. These monitors remain separate and isolated from the software typically controlling the system, but use the same sensor information. They are embedded in the circuitry and act as their own small, task-specific processors watching to make sure a particular rule is not violated; otherwise, they take control of the system and force corrective behavior. The monitors are added to a consumer off-the-shelf (COTS) drone to demonstrate their effectiveness. For every rule monitored, an override is triggered when they are violated. Their effectiveness depends on reliable sensor information as with any electronic component, and the completeness of the rules detailing these monitors.

Este trabalho investiga a viabilidade de se implantar no Brasil o veículo combinado de cinco eixos constituído de um cavalo mecânico mais dois semi-reboques acoplados por um dolly intermediário e chamado aqui de Duplo Semi-Reboque (DSR). Essa investigação inclui tanto aspectos econômicos (custos operacionais) quanto operacionais (densidade das cargas, rotas, demandas, veículos utilizados), tecnológicos (veículos e implementes), legais (pesos e dimensões), de segurança (estabilidade, dirigibilidade, risco de acidentes e impacto sobre o tráfego de outros veículos) e de inter-relação com a infra-estrutura rodoviária. Como a configuração analisada é largamente utilizada nos Estados Unidos, com o nome de twin trailer truck, faz-se uma ampla revisão da literatura norte-americana. O estudo apresenta as características técnicas do twin, levanta a legislação norte-americana de carga por eixo e mostra como a busca de produtividade e o aumento da carga volumosa conduziram à necessidade de veículos mais longos. Compila artigos sobre a estabilidade, a dirigibilidade e o impacto sobre o tráfego dos veículos longos combinados. Sintetiza pesquisas comparando taxas de acidentes dos veículos combinados com os caminhões convencionais. A maioria desses estudos conduz à conclusão de que, embora os twins possam degradar ligeiramente as condições de segurança de tráfego e aumentar o desgaste elos pavimentos, essa degradação é compensada pela redução do número de viagens e do custo do transporte. Conclui-se que o veículo seria economicamente viável no Brasil para substituir caminhões trucados em rotas de demanda limitada, e que poderia também economizar custos na substituição a veículos convencionais no transporte de cargas volumosas, sem provocar maiores impactos sobre a segurança operacional. Pesquisa com frotistas mostra que quase 50% das transportadoras de carga fracionada operam cargas de densidade compatível com o DSR. A introdução do veículo, no entanto, enfrenta fortes obstáculos legais e exigiria mudança profunda na legislação dos veículos combinados longos. / This paper investigates the feasibility of introducing the American twin trailer truck in the Brazilian road transport network. The twin is a five axle configuration with one tractor and two semi-trailers, coupled by an intermediate dolly. The investigation embraces not only economic questions (operational costs), but also operational aspects (freight density and volume, vehicle choice, line extension etc), technological questions (vehicles, trailers and dollies), weights and dimensions legislation, safety impacts (handling and stability, impact of traffic operations and statistic studies of accident rates) and the twin\'s interface with the highway facilities. The American and Canadian studies about twins are reviewed. The paper presents the technical characteristics of twins, the american weights and dimensions legislation and shows how the claim for more productivity in the transport industry and the low density freight growth have induced the use of longer combinations. The study compiles the main results presented in the literature about handling, stability and the twin trailer impact on the highway traffic and analyzes statistics comparing doubles with semi-trailer accident rates. The literature review leads to the conclusion that, althrough the twins could degrade slightly the vehicle traffic safety performance and accelerate the pavement wear, this degradation is overwhelmed by the reduction of the number of vehicles on the roads and direct and indirect transportation costs. The introduction of the win trailer truck in Brazil could be advantageous in order to replace tandem trucks on low demand routes. The savings in terminal times and the higher capacitiy of this configuration would cut costs as compared to the straight truck, semi-trailer and truck-and-trailer configurations, without relevant deterioration of the operational safety. The results of a large sample with brazilian LTL companies show that almost 50% of them operate with a freight density that would be ideal for twins. The twin\'s introduction, however, faces strong legal impediments in some markets, and only would be feasible if deep changes in the Brazilian weight and dimension regulations would be undertaken.

Este trabalho investiga a viabilidade de se implantar no Brasil o veículo combinado de cinco eixos constituído de um cavalo mecânico mais dois semi-reboques acoplados por um dolly intermediário e chamado aqui de Duplo Semi-Reboque (DSR). Essa investigação inclui tanto aspectos econômicos (custos operacionais) quanto operacionais (densidade das cargas, rotas, demandas, veículos utilizados), tecnológicos (veículos e implementes), legais (pesos e dimensões), de segurança (estabilidade, dirigibilidade, risco de acidentes e impacto sobre o tráfego de outros veículos) e de inter-relação com a infra-estrutura rodoviária. Como a configuração analisada é largamente utilizada nos Estados Unidos, com o nome de twin trailer truck, faz-se uma ampla revisão da literatura norte-americana. O estudo apresenta as características técnicas do twin, levanta a legislação norte-americana de carga por eixo e mostra como a busca de produtividade e o aumento da carga volumosa conduziram à necessidade de veículos mais longos. Compila artigos sobre a estabilidade, a dirigibilidade e o impacto sobre o tráfego dos veículos longos combinados. Sintetiza pesquisas comparando taxas de acidentes dos veículos combinados com os caminhões convencionais. A maioria desses estudos conduz à conclusão de que, embora os twins possam degradar ligeiramente as condições de segurança de tráfego e aumentar o desgaste elos pavimentos, essa degradação é compensada pela redução do número de viagens e do custo do transporte. Conclui-se que o veículo seria economicamente viável no Brasil para substituir caminhões trucados em rotas de demanda limitada, e que poderia também economizar custos na substituição a veículos convencionais no transporte de cargas volumosas, sem provocar maiores impactos sobre a segurança operacional. Pesquisa com frotistas mostra que quase 50% das transportadoras de carga fracionada operam cargas de densidade compatível com o DSR. A introdução do veículo, no entanto, enfrenta fortes obstáculos legais e exigiria mudança profunda na legislação dos veículos combinados longos. / This paper investigates the feasibility of introducing the American twin trailer truck in the Brazilian road transport network. The twin is a five axle configuration with one tractor and two semi-trailers, coupled by an intermediate dolly. The investigation embraces not only economic questions (operational costs), but also operational aspects (freight density and volume, vehicle choice, line extension etc), technological questions (vehicles, trailers and dollies), weights and dimensions legislation, safety impacts (handling and stability, impact of traffic operations and statistic studies of accident rates) and the twin\'s interface with the highway facilities. The American and Canadian studies about twins are reviewed. The paper presents the technical characteristics of twins, the american weights and dimensions legislation and shows how the claim for more productivity in the transport industry and the low density freight growth have induced the use of longer combinations. The study compiles the main results presented in the literature about handling, stability and the twin trailer impact on the highway traffic and analyzes statistics comparing doubles with semi-trailer accident rates. The literature review leads to the conclusion that, althrough the twins could degrade slightly the vehicle traffic safety performance and accelerate the pavement wear, this degradation is overwhelmed by the reduction of the number of vehicles on the roads and direct and indirect transportation costs. The introduction of the win trailer truck in Brazil could be advantageous in order to replace tandem trucks on low demand routes. The savings in terminal times and the higher capacitiy of this configuration would cut costs as compared to the straight truck, semi-trailer and truck-and-trailer configurations, without relevant deterioration of the operational safety. The results of a large sample with brazilian LTL companies show that almost 50% of them operate with a freight density that would be ideal for twins. The twin\'s introduction, however, faces strong legal impediments in some markets, and only would be feasible if deep changes in the Brazilian weight and dimension regulations would be undertaken.

A main thrust of this thesis is to develop and explore linearization-based numeric-analytic integration techniques in the context of stochastically driven nonlinear oscillators of relevance in structural dynamics. Unfortunately, unlike the case of deterministic oscillators, available numerical or numeric-analytic integration schemes for stochastically driven oscillators, often modelled through stochastic differential equations (SDE-s), have significantly poorer numerical accuracy. These schemes are generally derived through stochastic Taylor expansions and the limited accuracy results from difficulties in evaluating the multiple stochastic integrals. We propose a few higher-order methods based on the stochastic version of transversal linearization and another method of linearizing the nonlinear drift field based on a Girsanov change of measures. When these schemes are implemented within a Monte Carlo framework for computing the response statistics, one typically needs repeated simulations over a large ensemble. The statistical error due to the finiteness of the ensemble (of size N, say)is of order 1/√N, which implies a rather slow convergence as N→∞. Given the prohibitively large computational cost as N increases, a variance reduction strategy that enables computing accurate response statistics for small N is considered useful. This leads us to propose a weak variance reduction strategy. Finally, we use the explicit derivative-free linearization techniques for state and parameter estimations for structural systems using the extended Kalman filter (EKF). A two-stage version of the EKF (2-EKF) is also proposed so as to account for errors due to linearization and unmodelled dynamics. In Chapter 2, we develop higher order locally transversal linearization (LTL) techniques for strong and weak solutions of stochastically driven nonlinear oscillators. For developing the higher-order methods, we expand the non-linear drift and multiplicative diffusion fields based on backward Euler and Newmark expansions while simultaneously satisfying the original vector field at the forward time instant where we intend to find the discretized solution. Since the non-linear vector fields are conditioned on the solution we wish to determine, the methods are implicit. We also report explicit versions of such linearization schemes via simple modifications. Local error estimates are provided for weak solutions. Weak linearized solutions enable faster computation vis-à-vis their strong counterparts. In Chapter 3, we propose another weak linearization method for non-linear oscillators under stochastic excitations based on Girsanov transformation of measures. Here, the non-linear drift vector is appropriately linearized such that the resulting SDE is analytically solvable. In order to account for the error in replacing of non-linear drift terms, the linearized solutions are multiplied by scalar weighting function. The weighting function is the solution of a scalar SDE(i.e.,Radon-Nikodym derivative). Apart from numerically illustrating the method through applications to non-linear oscillators, we also use the Girsanov transformation of measures to correct the truncation errors in lower order discretizations. In order to achieve efficiency in the computation of response statistics via Monte Carlo simulation, we propose in Chapter 4 a weak variance reduction strategy such that the ensemble size is significantly reduced without seriously affecting the accuracy of the predicted expectations of any smooth function of the response vector. The basis of the variance reduction strategy is to appropriately augment the governing system equations and then weakly replace the associated stochastic forcing functions through variance-reduced functions. In the process, the additional computational cost due to system augmentation is generally far less besides the accrued advantages due to a drastically reduced ensemble size. The variance reduction scheme is illustrated through applications to several non-linear oscillators, including a 3-DOF system. Finally, in Chapter 5, we exploit the explicit forms of the LTL techniques for state and parameters estimations of non-linear oscillators of engineering interest using a novel derivative-free EKF and a 2-EKF. In the derivative-free EKF, we use one-term, Euler and Newmark replacements for linearizations of the non-linear drift terms. In the 2-EKF, we use bias terms to account for errors due to lower order linearization and unmodelled dynamics in the mathematical model. Numerical studies establish the relative advantages of EKF-DLL as well as 2-EKF over the conventional forms of EKF. The thesis is concluded in Chapter 6 with an overall summary of the contributions made and suggestions for future research.

Development of dynamic state estimation techniques and their applications in problems of identification in structural engineering have been taken up. The thrust of the study has been the identification of structural systems that exhibit nonlinear behavior, mainly in the form of constitutive and geometric nonlinearities. Methods encompassing both linearization based strategies and those involving nonlinear filtering have been explored. The applications of derivative-free locally transversal linearization (LTL) and multi-step transversal linearization (MTrL) schemes for developing newer forms of the extended Kalman filter (EKF) algorithm have been explored. Apart from the inherent advantages of these methods in avoiding gradient calculations, the study also demonstrates their superior numerical accuracy and considerably less sensitivity to the choice of step sizes. The range of numerical illustrations covers SDOF as well as MDOF oscillators with time-invariant parameters and those with discontinuous temporal variations. A new form of the sequential importance sampling (SIS) filter is developed which explores the scope of the existing SIS filters to cover nonlinear measurement equations and more general forms of noise involving multiplicative and (or) Gaussian/ non-Gaussian noises. The formulation of this method involves Ito-Taylor’s expansions of the nonlinear functions in the measurement equation and the development of the ideal ispdf while accounting for the non-Gaussian terms appearing in the governing equation. Numerical illustrations on parameter identification of a few nonlinear oscillators and a geometrically nonlinear Euler–Bernoulli beam reveal a remarkably improved performance of the proposed methods over one of the best known algorithms, i.e. the unscented particle filter. The study demonstrates the applicability of diverse range of mathematical tools including Magnus’ functional expansions, theory of SDE-s, Ito-Taylor’s expansions and simulation and characterization of the non-Gaussian random variables to the problem of nonlinear structural system identification.

Le développement croissant des réseaux et en particulier l'Internet a considérablement développé l'écart entre les systèmes d'information hétérogènes. En faisant une analyse sur les études de l'interopérabilité des systèmes d'information hétérogènes, nous découvrons que tous les travaux dans ce domaine tendent à la résolution des problèmes de l'hétérogénéité sémantique. Le W3C (World Wide Web Consortium) propose des normes pour représenter la sémantique par l'ontologie. L'ontologie est en train de devenir un support incontournable pour l'interopérabilité des systèmes d'information et en particulier dans la sémantique. La structure de l'ontologie est une combinaison de concepts, propriétés et relations. Cette combinaison est aussi appelée un graphe sémantique. Plusieurs langages ont été développés dans le cadre du Web sémantique et la plupart de ces langages utilisent la syntaxe XML (eXtensible Meta Language). Les langages OWL (Ontology Web Language) et RDF (Resource Description Framework) sont les langages les plus importants du web sémantique, ils sont basés sur XML.Le RDF est la première norme du W3C pour l'enrichissement des ressources sur le Web avec des descriptions détaillées et il augmente la facilité de traitement automatique des ressources Web. Les descriptions peuvent être des caractéristiques des ressources, telles que l'auteur ou le contenu d'un site web. Ces descriptions sont des métadonnées. Enrichir le Web avec des métadonnées permet le développement de ce qu'on appelle le Web Sémantique. Le RDF est aussi utilisé pour représenter les graphes sémantiques correspondant à une modélisation des connaissances spécifiques. Les fichiers RDF sont généralement stockés dans une base de données relationnelle et manipulés en utilisant le langage SQL ou les langages dérivés comme SPARQL. Malheureusement, cette solution, bien adaptée pour les petits graphes RDF n'est pas bien adaptée pour les grands graphes RDF. Ces graphes évoluent rapidement et leur adaptation au changement peut faire apparaître des incohérences. Conduire l'application des changements tout en maintenant la cohérence des graphes sémantiques est une tâche cruciale et coûteuse en termes de temps et de complexité. Un processus automatisé est donc essentiel. Pour ces graphes RDF de grande taille, nous suggérons une nouvelle façon en utilisant la vérification formelle " Le Model checking ".Le Model checking est une technique de vérification qui explore tous les états possibles du système. De cette manière, on peut montrer qu'un modèle d'un système donné satisfait une propriété donnée. Cette thèse apporte une nouvelle méthode de vérification et d'interrogation de graphes sémantiques. Nous proposons une approche nommé ScaleSem qui consiste à transformer les graphes sémantiques en graphes compréhensibles par le model checker (l'outil de vérification de la méthode Model checking). Il est nécessaire d'avoir des outils logiciels permettant de réaliser la traduction d'un graphe décrit dans un formalisme vers le même graphe (ou une adaptation) décrit dans un autre formalisme

Le développement croissant des réseaux et en particulier l'Internet a considérablement développé l'écart entre les systèmes d'information hétérogènes. En faisant une analyse sur les études de l'interopérabilité des systèmes d'information hétérogènes, nous découvrons que tous les travaux dans ce domaine tendent à la résolution des problèmes de l'hétérogénéité sémantique. Le W3C (World Wide Web Consortium) propose des normes pour représenter la sémantique par l'ontologie. L'ontologie est en train de devenir un support incontournable pour l'interopérabilité des systèmes d'information et en particulier dans la sémantique. La structure de l'ontologie est une combinaison de concepts, propriétés et relations. Cette combinaison est aussi appelée un graphe sémantique. Plusieurs langages ont été développés dans le cadre du Web sémantique et la plupart de ces langages utilisent la syntaxe XML (eXtensible Meta Language). Les langages OWL (Ontology Web Language) et RDF (Resource Description Framework) sont les langages les plus importants du web sémantique, ils sont basés sur XML.Le RDF est la première norme du W3C pour l'enrichissement des ressources sur le Web avec des descriptions détaillées et il augmente la facilité de traitement automatique des ressources Web. Les descriptions peuvent être des caractéristiques des ressources, telles que l'auteur ou le contenu d'un site web. Ces descriptions sont des métadonnées. Enrichir le Web avec des métadonnées permet le développement de ce qu'on appelle le Web Sémantique. Le RDF est aussi utilisé pour représenter les graphes sémantiques correspondant à une modélisation des connaissances spécifiques. Les fichiers RDF sont généralement stockés dans une base de données relationnelle et manipulés en utilisant le langage SQL ou les langages dérivés comme SPARQL. Malheureusement, cette solution, bien adaptée pour les petits graphes RDF n'est pas bien adaptée pour les grands graphes RDF. Ces graphes évoluent rapidement et leur adaptation au changement peut faire apparaître des incohérences. Conduire l’application des changements tout en maintenant la cohérence des graphes sémantiques est une tâche cruciale et coûteuse en termes de temps et de complexité. Un processus automatisé est donc essentiel. Pour ces graphes RDF de grande taille, nous suggérons une nouvelle façon en utilisant la vérification formelle « Le Model checking ».Le Model checking est une technique de vérification qui explore tous les états possibles du système. De cette manière, on peut montrer qu’un modèle d’un système donné satisfait une propriété donnée. Cette thèse apporte une nouvelle méthode de vérification et d’interrogation de graphes sémantiques. Nous proposons une approche nommé ScaleSem qui consiste à transformer les graphes sémantiques en graphes compréhensibles par le model checker (l’outil de vérification de la méthode Model checking). Il est nécessaire d’avoir des outils logiciels permettant de réaliser la traduction d’un graphe décrit dans un formalisme vers le même graphe (ou une adaptation) décrit dans un autre formalisme / The increasing development of networks and especially the Internet has greatly expanded the gap between heterogeneous information systems. In a review of studies of interoperability of heterogeneous information systems, we find that all the work in this area tends to be in solving the problems of semantic heterogeneity. The W3C (World Wide Web Consortium) standards proposed to represent the semantic ontology. Ontology is becoming an indispensable support for interoperability of information systems, and in particular the semantics. The structure of the ontology is a combination of concepts, properties and relations. This combination is also called a semantic graph. Several languages have been developed in the context of the Semantic Web. Most of these languages use syntax XML (eXtensible Meta Language). The OWL (Ontology Web Language) and RDF (Resource Description Framework) are the most important languages of the Semantic Web, and are based on XML.RDF is the first W3C standard for enriching resources on the Web with detailed descriptions, and increases the facility of automatic processing of Web resources. Descriptions may be characteristics of resources, such as the author or the content of a website. These descriptions are metadata. Enriching the Web with metadata allows the development of the so-called Semantic Web. RDF is used to represent semantic graphs corresponding to a specific knowledge modeling. RDF files are typically stored in a relational database and manipulated using SQL, or derived languages such as SPARQL. This solution is well suited for small RDF graphs, but is unfortunately not well suited for large RDF graphs. These graphs are rapidly evolving, and adapting them to change may reveal inconsistencies. Driving the implementation of changes while maintaining the consistency of a semantic graph is a crucial task, and costly in terms of time and complexity. An automated process is essential. For these large RDF graphs, we propose a new way using formal verification entitled "Model Checking".Model Checking is a verification technique that explores all possible states of the system. In this way, we can show that a model of a given system satisfies a given property. This thesis provides a new method for checking and querying semantic graphs. We propose an approach called ScaleSem which transforms semantic graphs into graphs understood by the Model Checker (The verification Tool of the Model Checking method). It is necessary to have software tools to perform the translation of a graph described in a certain formalism into the same graph (or adaptation) described in another formalism