First Assignment for AES Course:
Modelling Bluetooth Device Discovery in Uppaal
Background
Our society increasingly depends on the correct functioning of modern
communication technology. Most prominent are (mobile) phones and Internet,
but there are also networks in modern cars, trains, and airplanes, and
the new generation of consumer electronics allows all sorts of devices
to communicate with each other.
The most important and most often used protocols that describe the operation
of these networks are standardized.
Examples of this are the Internet protocol (TCP/IP) and all its derivatives,
FireWire/iLink (IEEE 1394), HAVi, WAP and Bluetooth.
Due to a combination of factors, the complexity of these protocol standards
is often very high: rapid changes in the capabilities of the underlying
hardware, the fact that often many (industrial) parties are involved in
standardization, each with its own interests, and market demands
to extend the functionality of the protocol.
Since these standards serve as a guide to implementors from many different
companies, with very different backgrounds, it is vital that standards only
allow for one clear interpretation, are complete and ensure the required
functionality for each implementation.
For most protocol standards this is clearly not the case. In fact, it is
surprising that protocols that are of such immense importance to our
society are typically written in informal language, with frequent ambiguities,
omissions and inconsistencies.
They also fail to state what properties are expected of a network running the
protocol, and what it means for an implementation to conform to a standard.
Bluetooth is a protocol which obviously
has great practical importance. For an introduction see e.g. the
Dutch or
English Wikipedia.
The official specification 2.0 of the protocol,
which is available though the Bluetooth website,
is long (2302 pages!), largely informal but appears to be of high quality.
Goal
The goal of this assignment is to pick one specific fragment of the Bluetooth
specification, namely device discovery, and to assess the quality of this specification fragment
by carefully studying the text and by constructing a formal model using Uppaal.
Instructions
A formal model of device discovery has been built before by
researchers from the
University of Birmingham using the probabilistic model checker PRISM.
The PRISM model (without probabilities) may serve as a basis for the Uppaal model.
Note however that the objective of the Birmingham case study was to show that PRISM
is useful for analysis, so their model abstracts quite a bit from the standard.
Also, their model is based on version 1.2 whereas we will be looking at version 2.0 of the
Bluetooth specification.
The actual description of the fragment is contained in Sections 1 and 2 of
Core System Package [Controller volume] Part B: Baseband Specification, i.e.,
pages 221-260 of the PDF file.
All participants should try to read this section before the course session
on March 16. On March 16 we will then discuss the text and try to come
up with a more detailled plan on how to proceed.