Verificação formal usando model checking para sistemas automotivos

Computer systems become complex, either because of their number of tasks, resource contention and / or accuracy, and aid in the human routine, but most of these are not properly tested and are susceptible to failure, which often entails rework, poor performance, expenses and threats to human life. F...

ver descrição completa

Autor principal: Silva, Renan Francisco Macarroni da
Formato: Trabalho de Conclusão de Curso (Graduação)
Idioma: Português
Publicado em: Universidade Tecnológica Federal do Paraná 2020
Assuntos:
Acesso em linha: http://repositorio.utfpr.edu.br/jspui/handle/1/15985
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id riut-1-15985
recordtype dspace
spelling riut-1-159852020-11-19T18:24:48Z Verificação formal usando model checking para sistemas automotivos Formal verification using model checking for automotive systems Silva, Renan Francisco Macarroni da Matos, Simone Nasser Santos, Max Mauro Matos, Simone Nasser Santos, Max Mauro Dias Alves, Gleifer Vaz Lacerda, Victor Schnepper Sistemas embarcados (Computadores) Indústria automobilística Teoria dos autômatos Embedded computer systems Automobile industry and trade Machine theory CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO Computer systems become complex, either because of their number of tasks, resource contention and / or accuracy, and aid in the human routine, but most of these are not properly tested and are susceptible to failure, which often entails rework, poor performance, expenses and threats to human life. Formal methods is an area of computing that works to minimize the impact that potential problems real-time systems have on those involved. Among the different approaches of this area, this work makes use of the formal verification of models, based on axioms and prepositions of temporal logic. Through the study of automotive software model present in the market, a formal verification was performed with the UPPAAL tool in an automotive window electric system. The approach comprises its modeling, simulation, specification evaluation and requirements verification. The result shows that the application of formal verification in real time systems identifies computational failures and offers high maintainability, provided it is correctly modeled. Sistemas computacionais tornam-se complexos, seja pelo seu número de tarefas, disputa de recurso e/ou pela sua precisão, e auxiliam na rotina do ser humano, porém a maioria desses não são devidamente testados e estão suscetíveis a falha, o que muitas vezes acarreta em retrabalho, mal desempenho, despesas e ameaças a vida humana. Métodos formais é uma área da computação que trabalha para minimizar o impacto que possíveis problemas que sistemas de tempo real oferecem aos envolvidos. Dentre as diferentes abordagens da área, este trabalho faz uso da verificação formal de modelos, embasado em axiomas e preposições da lógica temporal. Por meio do estudo de modelo de software automotivo presente no mercado, foi realizada uma verificação formal com a ferramenta UPPAAL em um sistema elétrico de janelas automotivo. A abordagem compreende sua modelagem, simulação, avaliação das especificações e verificação dos requisitos. O resultado mostra que a aplicação de verificação formal em sistemas de tempo real identifica falhas computacionais e oferece alta manutenibilidade, desde que este esteja corretamente modelado. 2020-11-19T18:24:48Z 2020-11-19T18:24:48Z 2019-11-12 bachelorThesis SILVA, Renan Francisco Macarroni da. Verificação formal usando model checking para sistemas automotivos. 2019. Trabalho de Conclusão de Curso (Bacharelado em Ciência da Computação) - Universidade Tecnológica Federal do Paraná, Ponta Grossa, 2019. http://repositorio.utfpr.edu.br/jspui/handle/1/15985 por openAccess application/pdf Universidade Tecnológica Federal do Paraná Ponta Grossa Brasil Departamento Acadêmico de Informática Ciência da Computação UTFPR
institution Universidade Tecnológica Federal do Paraná
collection RIUT
language Português
topic Sistemas embarcados (Computadores)
Indústria automobilística
Teoria dos autômatos
Embedded computer systems
Automobile industry and trade
Machine theory
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO
spellingShingle Sistemas embarcados (Computadores)
Indústria automobilística
Teoria dos autômatos
Embedded computer systems
Automobile industry and trade
Machine theory
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO
Silva, Renan Francisco Macarroni da
Verificação formal usando model checking para sistemas automotivos
description Computer systems become complex, either because of their number of tasks, resource contention and / or accuracy, and aid in the human routine, but most of these are not properly tested and are susceptible to failure, which often entails rework, poor performance, expenses and threats to human life. Formal methods is an area of computing that works to minimize the impact that potential problems real-time systems have on those involved. Among the different approaches of this area, this work makes use of the formal verification of models, based on axioms and prepositions of temporal logic. Through the study of automotive software model present in the market, a formal verification was performed with the UPPAAL tool in an automotive window electric system. The approach comprises its modeling, simulation, specification evaluation and requirements verification. The result shows that the application of formal verification in real time systems identifies computational failures and offers high maintainability, provided it is correctly modeled.
format Trabalho de Conclusão de Curso (Graduação)
author Silva, Renan Francisco Macarroni da
author_sort Silva, Renan Francisco Macarroni da
title Verificação formal usando model checking para sistemas automotivos
title_short Verificação formal usando model checking para sistemas automotivos
title_full Verificação formal usando model checking para sistemas automotivos
title_fullStr Verificação formal usando model checking para sistemas automotivos
title_full_unstemmed Verificação formal usando model checking para sistemas automotivos
title_sort verificação formal usando model checking para sistemas automotivos
publisher Universidade Tecnológica Federal do Paraná
publishDate 2020
citation SILVA, Renan Francisco Macarroni da. Verificação formal usando model checking para sistemas automotivos. 2019. Trabalho de Conclusão de Curso (Bacharelado em Ciência da Computação) - Universidade Tecnológica Federal do Paraná, Ponta Grossa, 2019.
url http://repositorio.utfpr.edu.br/jspui/handle/1/15985
_version_ 1805312447549014016
score 10,814766