A Formal Analysis of Bluetooth Device Discovery

Abstract. This paper presents a formal analysis of the device discovery phase of the Bluetooth wireless communication protocol. The performance of this process is the result of a complex interaction between several devices, some of which exhibit random behaviour. We use probabilistic model checking and, in particular, the tool PRISM to compute the best and worst case expected time for device discovery. We illustrate the utility of performing an exhaustive, low-level analysis to produce exact results in contrast to simulation techniques, where additional probabilistic assumptions must be made. We demonstrate an example of how seemingly innocuous assumptions can lead to incorrect performance estimations. We also analyse the effectiveness of improvements

• Type: Conference
• Year: 2004
• Where: ISOLA
• Authors: Marie Duflot, Marta Z. Kwiatkowska, Gethin Norman, David Parker
• Keywords: Additional Probabilistic Assumptions, Device Discovery, Device Discovery Phase, ISOLA 2004