www.prismmodelchecker.org
[DKNP06] Marie Duflot, Marta Kwiatkowska, Gethin Norman and David Parker. A Formal Analysis of Bluetooth Device Discovery. International Journal on Software Tools for Technology Transfer (STTT), 8(6), pages 621 - 632, Springer-Verlag. November 2006. [ps.gz] [pdf] [bib] [Analyses device discovery in Bluetooth using PRISM.]
Downloads:  ps.gz ps.gz (104 KB)  pdf pdf (167 KB)  bib bib
Notes: For further details of this case study, see this web page. The original publication is available at www.springerlink.com.
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 performance of device discovery: the expected time for the process to complete and the expected power consumption. 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 made between versions 1.1 and 1.2 of the Bluetooth specification.

Publications