| dc.description | RESUMEN
Durante las última década las expectativas y realidades en torno al acceso de última milla de banda ancha por medio inalámbrico han creado una ventana de oportunidades para fabricantes, integradores y prestadores de servicios. Hoy por hoy uno de los términos asociados con esta tecnología es IEEE 802.16. Los lineamientos de este estándar están dirigidos a la prestación de gran ancho de banda de manera inalámbrica para voz y datos para el ámbito residencial como empresarial. Sin embargo, la especificación del estándar IEEE 802.16 proporciona una descripción narrativa del protocolo sin ningún uso de técnicas formales. Así, algunas partes del documento pueden ser ambiguas, difíciles de entender, e imprecisas, especialmente en cuanto al mecanismo de retransmisión de bloques ARQ, que forma parte de la funcionalidad de la capa MAC. La implementación de este mecanismo es la única referencia para una validación del mismo.
Este trabajo modela el mecanismo de retransmisión de bloques ARQ usando una técnica formal conocida como Redes de Petri Coloreadas (CPNs). Los pasos siguientes resumen el proceso de verificación de la operación ARQ. Primero, la especificación de la operación ARQ derivada de la descripción del estándar. En segundo lugar, se modela la operación ARQ usando CPNs. Por último, se realiza el análisis basado en el método del gráfico de estado, cuyos resultados son comparados contra las propiedades de las CPNs. El resultado de este trabajo muestra que no hay ningún problema funcional significativo y la operación ARQ funciona según lo esperado, bajo las asunciones de modelado y de análisis.
Palabras Claves: Redes de Petri, CPNs, operación ARQ, gráfico de estado, capa MAC | |
