Utilização de model checking na verificação formal de um protocolo de rede full duplex sem fio
Ensuring the correct behavior of systems is no trivial task. Formal methods have been used in industrial and scientific applications to ensure proper working. Model checking is a modelbased formal method that recently has grown in popularity due to its considerable advantages such as solid mathemati...
| Autor principal: | Pereira Júnior, Matheus |
|---|---|
| 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/15930 |
| Tags: |
Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
|
| Resumo: |
Ensuring the correct behavior of systems is no trivial task. Formal methods have been used in industrial and scientific applications to ensure proper working. Model checking is a modelbased formal method that recently has grown in popularity due to its considerable advantages such as solid mathematical-logical foundation and counter-example generation, though it suffers from the state-explosion problem. Models are based on formalisms such as transition systems and Markov chains. Among these, timed automata is widely used to model real time systems and communication protocols since it has a natural way of expressing continuous temporal behavior. Properties of a model are formally specified through temporal logics including LTL and CTL. Examples of properties include deadlock freedom e guaranted function execution of given functionalities. Model checkers are tools that apply the model checking process. SPIN, PRISM e UPPAAL are examples. In this work a full duplex MAC protocol is modeled and verified using UPPAAL. Properties like successful completion of full duplex transmissions and an ACK sent for each successfully completed transmission are verified. |
|---|