1. Repositório Institucional da Universidade Tecnológica Federal do Paraná (RIUT)
  2. GRAD - Cursos de Graduação
  3. TCC - Trabalhos de Conclusão de Curso de Graduação
  4. Ponta Grossa
  5. PG - Ciência da Computação
Use este identificador para citar ou linkar para este item: http://repositorio.utfpr.edu.br/jspui/handle/1/15930
Registro completo de metadados
Campo DCValorIdioma
dc.creatorPereira Júnior, Matheus
dc.date.accessioned2020-11-19T18:23:08Z-
dc.date.available2020-11-19T18:23:08Z-
dc.date.issued2016-05-12
dc.identifier.citationPEREIRA JÚNIOR, Matheus. Utilização de model checking na verificação formal de um protocolo de rede full duplex sem fio. 2016. 93 f. Trabalho de Conclusão de Curso (Graduação) - Universidade Tecnológica Federal do Paraná, Ponta Grossa, 2016.pt_BR
dc.identifier.urihttp://repositorio.utfpr.edu.br/jspui/handle/1/15930-
dc.description.abstractEnsuring 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.pt_BR
dc.languageporpt_BR
dc.publisherUniversidade Tecnológica Federal do Paranápt_BR
dc.rightsopenAccesspt_BR
dc.subjectProtocolo de aplicação sem fio (Protocolo de rede de computador)pt_BR
dc.subjectIEEE 802.11 (Normas)pt_BR
dc.subjectSistemas de computaçãopt_BR
dc.subjectWireless Aplication Protocol (Computer network protocol)pt_BR
dc.subjectIEEE 802.11 (Standards)pt_BR
dc.subjectComputer systemspt_BR
dc.titleUtilização de model checking na verificação formal de um protocolo de rede full duplex sem fiopt_BR
dc.title.alternativeUsing model checking to formally verify a full duplex MAC protocol
dc.typebachelorThesispt_BR
dc.description.resumoAssegurar o correto funcionamento de sistemas é uma tarefa árdua. Métodos formais têm sido utilizados para tal finalidade. Model checking destaca-se como um método formal baseado em modelos utilizado por ter vantagens como sólida fundação matemática e lógica e geração de contra-exemplos, apesar de apresentar o problema da explosão de estados. Modelos são baseados em formalismos como sistemas de transição e cadeias de Markov. Dentre esses autômatos temporais, por apresentarem uma modelagem natural de aspectos temporais, são empregados para modelagem de sistemas em tempo real e protocolos de comunicação. As propriedades de um modelo são formalmente especificadas através de lógicas temporais como LTL e CTL. Exemplos de propriedade incluem ausência de deadlock e execução garantida de dadas funcionalidades. Model checkers são programas que aplicam o model checking. Exemplos incluem PRISM, SPIN e UPPAAL. No presente trabalho um protocolo de controle de acesso ao meio para redes full duplex sem fio é modelado através de autômato temporal e formalmente verificado usando o model checker UPPAAL. Propriedades como a ocorrência de uma transmissão full duplex completada com sucesso e envio de ACK para cada transmissão realizada foram verificadas.pt_BR
dc.degree.localPonta Grossapt_BR
dc.publisher.localPonta Grossapt_BR
dc.contributor.advisor1Alves, Gleifer Vaz
dc.contributor.referee1Alves, Gleifer Vaz
dc.contributor.referee2Borges, André Pinz
dc.contributor.referee3Almeida, Sheila Morais de
dc.publisher.countryBrasilpt_BR
dc.publisher.departmentDepartamento Acadêmico de Informáticapt_BR
dc.publisher.programCiência da Computaçãopt_BR
dc.publisher.initialsUTFPRpt_BR
dc.subject.cnpqCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAOpt_BR
Aparece nas coleções:PG - Ciência da Computação

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
PG_COCIC_2016_1_04.pdf1,88 MBAdobe PDFThumbnail
Visualizar/Abrir
Mostrar registro simples do item Recomendar este item Visualizar estatísticas


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.