Bluetooth es una tecnología de comunicación que proporciona comunicación entre dispositivos vía radio frecuencias en un área de alrededor de los 10 metros. La especificación de Bluetooth incluye un conjunto de protocolos, adoptados y propios, organizados de forma jerárquica. Uno de los protocolos propios de esta tecnología es el de bandabase. El establecimiento de una conexión es parte de la funciones de dicho protocolo. La especificación de este procedimiento es poco clara y ambigua y hace poco uso de herramientas para la descripción de protocolos tales como las tablas de estado. En este trabajo, las Redes de Petri Coloreadas (Coloured Petri Nets, CPNs), las cuales son una técnica formal, se utilizan para modelar el establecimiento de una conexión en un dispositivo Bluetooth maestro y en uno esclavo. Dicho modelo es entonces validado y depurado usando la técnica del espacio de estado. El análisis inicial muestra que el modelo se comporta acorde a lo esperado dadas las asunciones del modelo y las hechas para fines del análisis. La mayor contribución de este trabajo es el haber logrado una especificación clara y precisa del procedimiento a través del uso de la CPNs.