Probably the best device-checker in the world

A software tool developed at the University of Oxford is making computer-controlled devices and designs more reliable.

We are today on the verge of a new era in computing as information processing moves out of desktop computers and into the everyday objects that surround us. Bluetooth mobile phones can automatically sense each others’ presence and exchange information. Refrigerators that ‘know’ when they are nearly empty and order food deliveries via the internet are not far behind.

The future will hold many such devices with embedded systems, and their designers need to be able to understand how to optimise the way they operate, so that the probability of system failure or arriving at a ‘bad’ outcome – such as the failure of an inbuilt computer-controlled car braking system – can be minimised, even if it can never be eliminated.

Marta Kwiatkowska, Professor of Computing Systems at the University of Oxford has devised a software tool called PRISM that mathematically models such systems, calculating the probabilities of all possible outcomes to find out how reliable the system is. For example, applying PRISM to the protocol (set of rules) inside a Bluetooth-enabled mobile phone that allows it to detect other Bluetooth phones in the vicinity gives a probability that connection will be successful. It can also, for example, calculate the shortest and longest times that this is expected to take. Armed with this information, designers can modify the protocol to optimise performance.

PRISM’s other applications include assessing the likelihood of information leaks – what’s the probability that a PIN number can be guessed or ‘overheard’ during wireless communication, for example? Measuring these risks means that the protocols can be altered to minimise the chance of a PIN number being discovered.

The PRISM probabilistic model checker was made available worldwide as open source software (i.e. it is free to download) in 2001. So far, there have been over 20,000 downloads.

Funded by: The Engineering and Physical Sciences Research Council, the European Research Council, Microsoft Research Cambridge, QinetiQ, the Department of Trade and Industry, DARPA, and the British Council.