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...
| 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!
|
| Resumo: |
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. |
|---|