Fechar
Metadados

@MastersThesis{Pereira:2018:MoChPr,
               author = "Pereira, Viny Cesar",
                title = "Model checking probabil{\'{\i}}stico para apoiar a 
                         mitiga{\c{c}}{\~a}o de evento de falta {\'u}nica em Field 
                         Programmable Gate Arrays (FPGAs)",
               school = "Instituto Nacional de Pesquisas Espaciais (INPE)",
                 year = "2018",
              address = "S{\~a}o Jos{\'e} dos Campos",
                month = "2018-03-28",
             keywords = "verifica{\c{c}}{\~a}o formal, model checking 
                         probabil{\'{\i}}stico, single event upset, field programmable 
                         gate array, formal verification, probabilistic model checking.",
             abstract = "O uso de dispositivos l{\'o}gicos program{\'a}veis como Field 
                         Programmable Gate Arrays (FPGAs) em aplica{\c{c}}{\~o}es 
                         espaciais cresceu fortemente nos {\'u}ltimos anos devido {\`a} 
                         sua flexibilidade, custo de desenvolvimento e desempenho. 
                         Por{\'e}m, existe uma exposi{\c{c}}{\~a}o excessiva aos raios 
                         c{\'o}smicos presentes no ambiente e os efeitos da 
                         radia{\c{c}}{\~a}o podem causar erros transientes, quando 
                         part{\'{\i}}culas carregadas atingem a superf{\'{\i}}cie dos 
                         componentes. Tais efeitos s{\~a}o chamados de Single Event 
                         Effects (SEEs), que, em sua forma n{\~a}o destrutiva conhecida 
                         como Evento de Falta {\'U}nica (Single Event Upset (SEU)), pode 
                         atingir as c{\'e}lulas de mem{\'o}ria e causar uma invers{\~a}o 
                         no valor l{\'o}gico armazenado, ou seja, um bit flip. Diversas 
                         t{\'e}cnicas de detec{\c{c}}{\~a}o, mitiga{\c{c}}{\~a}o e 
                         corre{\c{c}}{\~a}o de SEU surgiram no passado como forma de 
                         evitar falhas, mas a maioria dos testes presentes na literatura 
                         foram conduzidos ap{\'o}s implementar as t{\'e}cnicas em FPGAs e 
                         simular os upsets com ferramentas de inje{\c{c}}{\~a}o de 
                         falhas, o que pode ser uma abordagem custosa, j{\'a} que os 
                         resultados s{\'o} s{\~a}o apresentados ao final das 
                         simula{\c{c}}{\~o}es. Por outro lado, modelos 
                         estoc{\'a}sticos/probabil{\'{\i}}sticos podem ser utilizados 
                         nos est{\'a}gios iniciais de um projeto sem a necessidade de 
                         implementa{\c{c}}{\~a}o, com grande potencial para amortizar o 
                         custo do projeto como um todo. Um dos m{\'e}todos que lida com 
                         sistemas de comportamento estoc{\'a}stico {\'e} o Model Checking 
                         Probabil{\'{\i}}stico, o qual {\'e} capaz de garantir, de 
                         acordo com uma probabilidade especificada, a corretude do sistema. 
                         Essa disserta{\c{c}}{\~a}o de mestrado investiga a viabilidade, 
                         no contexto de aplica{\c{c}}{\~o}es espaciais, da 
                         utiliza{\c{c}}{\~a}o de Model Checking Probabil{\'{\i}}stico 
                         para determinar, dentre um conjunto de solu{\c{c}}{\~o}es, qual 
                         seria a melhor t{\'e}cnica de mitiga{\c{c}}{\~a}o de SEU em 
                         FPGAs SRAM. Para isso, as t{\'e}cnicas de Scrubbing, TMR e 
                         c{\'o}digo de Hamming foram modeladas via Model Checking 
                         Probabil{\'{\i}}stico com a ferramenta PRISM. Os modelos foram 
                         comparados em dois estudos de caso, com caracter{\'{\i}}sticas 
                         de {\'o}rbita e tempos de miss{\~a}o distintos, considerando uma 
                         Xilinx Virtex-5 em ambos os tipos de ioniza{\c{c}}{\~a}o, direta 
                         e indireta. Considerando tr{\^e}s atributos de dependabilidade, 
                         disponibilidade, seguran{\c{c}}a e confiabilidade, as 
                         t{\'e}cnicas tamb{\'e}m foram implementadas e simuladas via 
                         ModelSim para obter compara{\c{c}}{\~o}es com os modelos 
                         probabil{\'{\i}}sticos desenvolvidos. As an{\'a}lises dos 
                         modelos mostram que, em termos de disponibilidade, o c{\'o}digo 
                         de Hamming apresentou o melhor desempenho mantendo o sistema por 
                         mais tempo em modo operacional mesmo com a pior taxa de falhas. Na 
                         confiabilidade, o que mais afetou o Scrubbing foi o tamanho do 
                         intervalo entre as corre{\c{c}}{\~o}es enquanto a 
                         seguran{\c{c}}a est{\'a} mais relacionada com a taxa de 
                         cobertura. O TMR apresentou os piores resultados pois permite que 
                         os upsets se acumulem e deve ser combinado com alguma t{\'e}cnica 
                         de corre{\c{c}}{\~a}o, como o c{\'o}digo de Hamming ou 
                         Scrubbing. J{\'a} os resultados da compara{\c{c}}{\~a}o com a 
                         simula{\c{c}}{\~a}o funcional mostram que as 
                         condi{\c{c}}{\~o}es de {\'o}rbita e tempos de miss{\~a}o 
                         s{\~a}o fatores impactantes na precis{\~a}o dos modelos e devem 
                         ser considerados. Por fim, {\'e} poss{\'{\i}}vel confirmar a 
                         viabilidade do uso de Model Checking Probabil{\'{\i}}stico pois, 
                         na maioria dos casos, tal abordagem apresentou resultados 
                         pr{\'o}ximos aos obtidos com simula{\c{c}}{\~a}o funcional. 
                         ABSTRACT: The use of programmable logic devices such as Field 
                         Programmable Gate Arrays (FPGAs) in space applications has grown 
                         strongly in recent years due to its flexibility, development cost 
                         and performance. However, there is excessive exposure to the 
                         cosmic rays present in the environment and the effects of 
                         radiation can cause transient errors, when charged particles reach 
                         the surface of the components. These effects are called Single 
                         Event Effects (SEEs), which in their non-destructive form known as 
                         Single Event Upset (SEU) can reach the memory cells and cause a 
                         reversal in the stored logical value, i.e. a bit flip. Several 
                         techniques of detection, mitigation and correction of SEU have 
                         appeared in the past as a way of avoiding failures, but most of 
                         the tests in the literature were conducted after implementing the 
                         techniques in FPGAs and simulate upsets with fault injection 
                         tools, which can be a costly approach, since the results are only 
                         presented at the end of the simulations. On the other hand, 
                         stochastic/probabilistic models can be used in the early stages of 
                         design without the need of implementation, with great potential to 
                         amortize the cost of the design as a whole. One of the methods 
                         that deals with stochastic behavior systems is the Probabilistic 
                         Model Checking, which is able to guarantee, within a specified 
                         probability, the correctness of the system. This masters 
                         dissertation investigates the feasibility, in the context of space 
                         applications, the use of Probabilistic Model Checking to 
                         determine, among a set of solutions, what would be the best SEU 
                         mitigation technique in SRAM FPGAs. For this, the Scrubbing, TMR 
                         and Hamming code techniques were modeled using Probabilistic Model 
                         Checking within the PRISM tool. The models were compared in two 
                         case studies, with distinct orbit characteristics and mission 
                         times, considering a Xilinx Virtex-5 in both direct and indirect 
                         types of ionization. Considering three attributes of 
                         dependability, availability, safety and reliability, the 
                         techniques were also implemented and simulated via ModelSim to 
                         obtain comparisons with the developed probabilistic models. The 
                         analyzes of the models show that in terms of availability, the 
                         Hamming code presented the best performance by keeping the system 
                         longer in operational mode even with the worst failure rate. In 
                         reliability, what most affected Scrubbing was the size of the 
                         interval between corrections while safety is more related to the 
                         coverage rate. TMR showed the worst results because it allows 
                         upsets to accumulate and must be combined with some correction 
                         technique such as Hamming code or Scrubbing. The results of the 
                         comparison with the functional simulation show that the orbit 
                         conditions and mission times are impacting factors on the accuracy 
                         of models and should be considered. Finally, it is possible to 
                         confirm the feasibility of using Probabilistic Model Checking 
                         because, in most cases, this approach showed similar results to 
                         those obtained with functional simulation.",
            committee = "Rosa, Reinaldo Roberto (presidente) and Santiago J{\'u}nior, 
                         Valdivino Alexandre de (orientador) and Manea, Silvio and D'Amore, 
                         Roberto",
         englishtitle = "Probabilistic model checking to support the mitigation of single 
                         event upset in Field Programmable Gate Arrays (FPGAs)",
             language = "pt",
                pages = "134",
                  ibi = "8JMKD3MGP3W34P/3QLQMU2",
                  url = "http://urlib.net/rep/8JMKD3MGP3W34P/3QLQMU2",
           targetfile = "publicacao.pdf",
        urlaccessdate = "23 nov. 2020"
}


Fechar