This dissertation shows that the bounded property verification of hardware Register Transfer Level (RTL) designs can be efficiently performed by precise abstract interpretation of a software representation of the RTL. The first part of this dissertation presents a novel framework for RTL verification using native software analyzers. To this end, we first present a translation of the hardware circuit expressed in Verilog RTL into the software in C called the software netlist. We then present the application of native software analyzers based on SAT/SMT-based decision procedures as well as abstraction-based techniques such as abstract interpretation for the formal verification of the software netlist design generated from the hardware RTL. In particular, we show that the path-based symbolic execution techniques, commonly used for automatic test case generation in system softwares, are also effective for proving bounded safety as well as detecting bugs in the software netlist designs. Furthermore, by means of experiments, we show that abstract interpretation techniques, commonly used for static program analysis, can also be used for bounded as well as unbounded safety property verification of the software netlist designs. However, the analysis using abstract interpretation shows high degree of imprecision on our benchmarks which is handled by manually guiding the analysis with various trace partitioning directives. The second part of this dissertation presents a new theoretical framework and a practical instantiation for automatically refining the precision of abstract interpretation using Conflict Driven Clause Learning (CDCL)-style analysis. The theoretical contribution is the abstract interpretation framework that generalizes CDCL to precise safety verification for automatic transformer refinement called Abstract Conflict Driven Learning for Safety (ACDLS). The practical contribution instantiates ACDLS over a template polyhedra abstract domain for bounded safety verification of the software netlist designs. We experimentally show that ACDLS is more efficient than a SAT-based analysis as well as sufficiently more precise than a commercial abstract interpreter.

Sistemas de transporte marítimo são essenciais para o Comércio Global, em especial, navios-tanques e seus centros de carga e descarga de produtos líquidos ou gasosos inflamáveis; portanto, é crucial entender como estes sistemas podem falhar, para que seus operadores sejam capazes de manter a sua capacidade de operação. É preciso que cada e toda análise quantitativa de risco compreenda algumas das atividades básicas que devem ser desenvolvidas, para permitir a quantificação dos riscos envolvidos e associados, na operação do sistema ou do processo. Basicamente, devem ser calculadas as probabilidades de ocorrência dos eventos indesejados identificados, bem como a magnitude de suas consequências. O objetivo deste trabalho é aferir se a técnica denominada Rede Bayesiana RB é a mais adequada, comparando-a com as técnicas de árvores de falhas e de eventos, para realizar uma Análise de Risco da operação ou processo de descarga de líquidos inflamáveis, como etanol anidro e/ou produtos petrolíferos, de um naviotanque para um terminal portuário específico Terminal de Granéis Líquidos TGL com foco na interface entre dois sistemas: o navio e o porto, observado o elemento humano, ou seja, o erro humano (Análise da Confiabilidade Humana). Além disso, será realizado um estudo das consequências do vazamento de um líquido inflamável transportado pelo navio, olhando para o pior cenário, a partir da ruptura da tubulação ou do compartimento do navio-tanque. A análise tem por base as recomendações da Organização Internacional Marítima OIM (em inglês, IMO). A OIM tem adotado a Avaliação Formal da Segurança AFS (em inglês, Formal Safety Assessment FSA), como seu modo oficial de receber as sugestões de seus membros para criar ou modificar qualquer regulamentação correlacionada. Este processo é composto de cinco passos que a OIM descreve na guia AFS (IMO, 2002). Este trabalho irá mostrar todas as etapas, mas irá focar, com especial atenção, a segunda etapa Risk Assessment, porque será aplicada ao caso sob análise, envolvendo o comportamento humano. Existem muitas técnicas e muito trabalho envolvido na estimação das probabilidades dos eventos. O mesmo ocorre para a avaliação de suas consequências. Uma vez definida a quantidade total de vazamento, um software poderá ser usado para calcular as consequências. O mesmo será feito para na Análise de Risco, utilizando RB, e, neste ponto, o trabalho apresenta uma nova contribuição. / Maritime transportation systems are essential for World Trade, in special, Tankers ships and yours loading and unloading facilities; therefore, it is crucial to understand how these systems may fail, to be able to maintain their capacity. It need that each and every quantitative risk assessment comprises some basic activities that have to be developed to allow the quantification of the risks involved in the operation of a system or process. Basically, it must be estimated the likelihood of the identified undesired events as well as the magnitude of their consequences. The objective of this study is to assess if the technique called Bayesian Networks BN is the best suited, with respect to the Fault Tree Analysis FTA and the Event Tree Analysis ETA, to perform an Risk Analysis of the operation or process of unloading of flammable bulk liquids, such as anhydrous ethanol and/or oil products, from a Tanker to a port terminal specified the Bulk Liquid Terminal BLT, focusing on the interface between the two systems: ship and port with the inclusion of the human factor, i.e., human error: Human Reliability Analysis HRA. Furthermore, a consequence analysis of a specific liquid bulk leakage will be performed, looking at the worst scenario case, from the rupture of a pipeline or tank from a Tanker. The analysis came from based on the recommendations of the International Maritime Organization IMO. The IMO has adopted the FSA (Formal Safety Assessment) as its official way of receiving suggestions of its members to create or modify any regulation correlated. It is a process composed by five steps that IMO has described in its Guidelines for FSA (IMO, 2002). This thesis will to show all steps, but will look carefully to step two (Risk Assessment) because it will be applied in the example situation, involving human behavior (HRA). There are many techniques and much work involved in the estimation of the likelihood of the events. The same occurs for the evaluation of their consequences. Once defined the total leaked quantity, software will be used to calculate the consequences. The same will be done to Risk Analysis, using BN, and at this point, the work is a new contribution.

Sistemas de transporte marítimo são essenciais para o Comércio Global, em especial, navios-tanques e seus centros de carga e descarga de produtos líquidos ou gasosos inflamáveis; portanto, é crucial entender como estes sistemas podem falhar, para que seus operadores sejam capazes de manter a sua capacidade de operação. É preciso que cada e toda análise quantitativa de risco compreenda algumas das atividades básicas que devem ser desenvolvidas, para permitir a quantificação dos riscos envolvidos e associados, na operação do sistema ou do processo. Basicamente, devem ser calculadas as probabilidades de ocorrência dos eventos indesejados identificados, bem como a magnitude de suas consequências. O objetivo deste trabalho é aferir se a técnica denominada Rede Bayesiana RB é a mais adequada, comparando-a com as técnicas de árvores de falhas e de eventos, para realizar uma Análise de Risco da operação ou processo de descarga de líquidos inflamáveis, como etanol anidro e/ou produtos petrolíferos, de um naviotanque para um terminal portuário específico Terminal de Granéis Líquidos TGL com foco na interface entre dois sistemas: o navio e o porto, observado o elemento humano, ou seja, o erro humano (Análise da Confiabilidade Humana). Além disso, será realizado um estudo das consequências do vazamento de um líquido inflamável transportado pelo navio, olhando para o pior cenário, a partir da ruptura da tubulação ou do compartimento do navio-tanque. A análise tem por base as recomendações da Organização Internacional Marítima OIM (em inglês, IMO). A OIM tem adotado a Avaliação Formal da Segurança AFS (em inglês, Formal Safety Assessment FSA), como seu modo oficial de receber as sugestões de seus membros para criar ou modificar qualquer regulamentação correlacionada. Este processo é composto de cinco passos que a OIM descreve na guia AFS (IMO, 2002). Este trabalho irá mostrar todas as etapas, mas irá focar, com especial atenção, a segunda etapa Risk Assessment, porque será aplicada ao caso sob análise, envolvendo o comportamento humano. Existem muitas técnicas e muito trabalho envolvido na estimação das probabilidades dos eventos. O mesmo ocorre para a avaliação de suas consequências. Uma vez definida a quantidade total de vazamento, um software poderá ser usado para calcular as consequências. O mesmo será feito para na Análise de Risco, utilizando RB, e, neste ponto, o trabalho apresenta uma nova contribuição. / Maritime transportation systems are essential for World Trade, in special, Tankers ships and yours loading and unloading facilities; therefore, it is crucial to understand how these systems may fail, to be able to maintain their capacity. It need that each and every quantitative risk assessment comprises some basic activities that have to be developed to allow the quantification of the risks involved in the operation of a system or process. Basically, it must be estimated the likelihood of the identified undesired events as well as the magnitude of their consequences. The objective of this study is to assess if the technique called Bayesian Networks BN is the best suited, with respect to the Fault Tree Analysis FTA and the Event Tree Analysis ETA, to perform an Risk Analysis of the operation or process of unloading of flammable bulk liquids, such as anhydrous ethanol and/or oil products, from a Tanker to a port terminal specified the Bulk Liquid Terminal BLT, focusing on the interface between the two systems: ship and port with the inclusion of the human factor, i.e., human error: Human Reliability Analysis HRA. Furthermore, a consequence analysis of a specific liquid bulk leakage will be performed, looking at the worst scenario case, from the rupture of a pipeline or tank from a Tanker. The analysis came from based on the recommendations of the International Maritime Organization IMO. The IMO has adopted the FSA (Formal Safety Assessment) as its official way of receiving suggestions of its members to create or modify any regulation correlated. It is a process composed by five steps that IMO has described in its Guidelines for FSA (IMO, 2002). This thesis will to show all steps, but will look carefully to step two (Risk Assessment) because it will be applied in the example situation, involving human behavior (HRA). There are many techniques and much work involved in the estimation of the likelihood of the events. The same occurs for the evaluation of their consequences. Once defined the total leaked quantity, software will be used to calculate the consequences. The same will be done to Risk Analysis, using BN, and at this point, the work is a new contribution.

In order to reach higher levels of autonomy in autonomous driving, it is important to consider potential occluded traffic participants. Current research has considered occlusion-aware autonomous driving in urban situations. However, no implementations have shown good performance in high velocity situations such as highway driving yet, since the current methods are too conservative in these situations and result in frequent excessive braking. In this work a method is proposed that tracks boundaries on the velocity states of potential hidden traffic using reachability analysis. It is proven that the method can guarantee collision-free trajectories for any, potentially hidden, traffic. The method is evaluated on cut-in scenarios retrieved from a dataset of recorded traffic. The results show that tracking the velocity bounds for potentially hidden traffic results in more efficient trajectories up to 18 km/h faster compared to existing occlusion-aware methods. While the method shows clear improvements, it does not always manage to establish a velocity bound and at times excessive braking still occurs. Further work is thus necessary to ensure consistently well-performing occlusion-aware highway driving. / För att nå högre nivåer av autonomi vid autonom körning är det viktigt att ta hänsyn till möjliga skymda trafikanter. Aktuell forskning har övervägt skymd-sikt-medveten autonom körning i urbana situationer. Emellertid har inga implementeringar visat bra prestanda i höghastighetssituationer såsom motorvägskörning ännu, eftersom de nuvarande metoderna är för konservativa i dessa situationer och resulterar i frekventa överdrivna inbromsningar. I detta arbete föreslås en metod som bestämmer gränser för hastighetstillstånden för möjlig skymd trafik med hjälp av nåbarhetsanalys. Det är bevisat att metoden kan garantera kollisionsfria banor för all möjlig skymd trafik. Metoden utvärderas på scenarier hämtade från ett dataset av registrerad trafik. Resultaten visar att bestämning av hastighetsgränserna för möjlig skymd trafik resulterar i effektivare banor upp till 18 km/h snabbare jämfört med befintliga skymd-sikt-medvetna-metoder. Även om metoden visar tydliga förbättringar, lyckas den inte alltid fastställa en hastighetsgräns och ibland förekommer fortfarande överdriven inbromsning. Ytterligare arbete är därför nödvändigt för att säkerställa konsekvent välpresterande motorvägskörning under skymd sikt.