Wireless protocol testing and validation supported by formal methods. A hands-on report

We apply formal testing and validation techniques and tools to analyse a configuration protocol for a Bluetooth Location Network (BLN). This network is composed by static Bluetooth nodes that establish a spontaneous network at system initialization. Once configured, BLN provides location services for location-aware or context-driven wireless environments, such as m-commerce networks or e-museums. BLN configuration was initially defined in natural language, and had passed some initial tests and simulation-based analysis. Formal methods have provided deeper understanding and discovered unexpected errors that may arise in some failure scenarios.