Verificação formal de um protocolo de rede sem fio através de model checking

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.contributorAlves, Gleifer Vaz-
Autor(es): dc.contributorQueiroz, Saulo Jorge Beltrão de-
Autor(es): dc.contributorAlves, Gleifer Vaz-
Autor(es): dc.contributorQueiroz, Saulo Jorge Beltrão de-
Autor(es): dc.contributorMonteiro, Tânia Lúcia-
Autor(es): dc.creatorRosas, Fabiano Almeida-
Data de aceite: dc.date.accessioned2022-02-21T21:25:43Z-
Data de disponibilização: dc.date.available2022-02-21T21:25:43Z-
Data de envio: dc.date.issued2020-11-18-
Data de envio: dc.date.issued2020-11-18-
Data de envio: dc.date.issued2014-11-11-
Fonte completa do material: dc.identifierhttp://repositorio.utfpr.edu.br/jspui/handle/1/15907-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/652415-
Descrição: dc.descriptionThis work consists of the application of the model checking technique to the formal specification, modeling and formal verification of the basic access method of the IEEE 802.11 standard medium access control protocol distributed coordination function (DCF). The modeling was made assuming nodes with saturated traffic and all stations starting at the same time. The purposed model admits typical configuration parameters of a IEEE 802.11 a/b/g network, such as number of nodes, channel width, data rate and packet size. Using the UPPAAL model checker, properties related to the minimum time needed for all the stations to transmit successfully were formally verified. This work intends to fill a gap that exists with relation to the formal modeling of the IEEE 802.11 DCF and serve as a basis for the formal verification of new 802.11 DCF variations.-
Descrição: dc.descriptionO presente trabalho trata da aplicação da técnica de model checking na especificação formal, modelagem e verificação formal do método de acesso básico da função de coordenação distribuída (DCF) do protocolo de controle de acesso ao meio do padrão IEEE 802.11. A modelagem foi feita assumindo nós com tráfego saturado e com todas as estações iniciando o seu funcionamento ao mesmo tempo. O modelo proposto admite a configuração de parâmetros típicos de uma rede IEEE 802.11 a/b/g, tais como número de nós, largura de canal, taxa de transmissão e tamanho de pacote. Utilizou-se do model checker UPPAAL e verificou-se propriedades relacionadas ao tempo mínimo necessário para que todas as estações possam transmitir com sucesso. Este trabalho pretende preencher uma lacuna existente com relação à modelagem formal do IEEE DCF e busca servir de base para a verificação formal de novas variações do 802.11 DCF.-
Formato: dc.formatapplication/pdf-
Idioma: dc.languagept_BR-
Publicador: dc.publisherUniversidade Tecnológica Federal do Paraná-
Publicador: dc.publisherPonta Grossa-
Publicador: dc.publisherBrasil-
Publicador: dc.publisherDepartamento Acadêmico de Informática-
Publicador: dc.publisherCiência da Computação-
Publicador: dc.publisherUTFPR-
Direitos: dc.rightsopenAccess-
Palavras-chave: dc.subjectRede de computador - Protocolos-
Palavras-chave: dc.subjectIEEE 802.11 (Normas)-
Palavras-chave: dc.subjectRedes locais sem fio-
Palavras-chave: dc.subjectComputer network protocols-
Palavras-chave: dc.subjectIEEE 802.11 (Standards)-
Palavras-chave: dc.subjectWireless LANs-
Palavras-chave: dc.subjectCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO-
Palavras-chave: dc.subjectBacharelado em Ciência da Computação-
Título: dc.titleVerificação formal de um protocolo de rede sem fio através de model checking-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositorio Institucional da UTFPR - RIUT

Não existem arquivos associados a este item.