https://repositorio.ufba.br/handle/ri/5259
Tipo: | Artigo de Periódico |
Título: | Specification and Verification of the IEEE 802.11 Medium Access Control and an Analysis of its Applicability to Real-Time Systems |
Título(s) alternativo(s): | Electronic Notes in Theoretical Computer Science |
Autor(es): | Barbosa, Frederico Jorge Ribeiro Andrade, Aline Maria Santos Silva, Flávio Morais de Assis Lima, George Marconi de Araújo |
Autor(es): | Barbosa, Frederico Jorge Ribeiro Andrade, Aline Maria Santos Silva, Flávio Morais de Assis Lima, George Marconi de Araújo |
Abstract: | The use domain of IEEE 802.11 networks has broadened to several types of application, including those that require quality of service and real-time guarantees. This trend in particular, has motivated the use of formal methods, not only to obtain a more precise knowledge of protocol properties, but also to specify and validate them. In this context, the contribution of this paper is twofold. First, we describe a formal specification of the IEEE 802.11 medium access control functions using UPPAAL, a freeware model checker tool. The described specification allowed us to verify important properties of these functions, taking into account both time and concurrency. Second, we report an experience of model checking a widely used and reasonably complex communication protocol, taking into consideration temporal requirements. |
Palavras-chave: | Formal Methods Real-Time Systems Wireless Network Software Reliability Software Specification |
URI: | http://www.repositorio.ufba.br/ri/handle/ri/5259 |
Data do documento: | 2008 |
Aparece nas coleções: | Artigo Publicado em Periódico (IC) |
Arquivo | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Specification and Verification of the IEEE 802.11 Medium Access Control and an Analysis of its Applicability to Real-Time Systems | 536,72 kB | Adobe PDF | Visualizar/Abrir |
Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.