Ubiquitous Computing at a Crossroads: Art, Science, Politics and Design 

January 6th and 7th 2009
Huxley Building, Imperial College London

Software verification for UbiComp

Marta Kwiatkowska, University of Oxford

Presentation slides

Software embedded in ubiquitous computing devices presents significant challenges due to high levels of concurrency, decentralisation and variability of context. This talk will give an overview of the challenges and how they may be tackled. It will also present recent results concerning a methodology and implementation for verifying ANSI-C programs that exhibit probabilistic behaviour, such as network failures. Our techniques target quantitative properties of software such as "the maximum probability of file-transfer failure" or "the minimum expected number of loop iterations". We build upon state-of-the-art techniques and tools, using SAT-based predicate abstraction, symbolic implementations of probabilistic model checking and components from GOTO-CC, SATABS and PRISM. Experimental results show that our approach performs very well in practice, successfully verifying actual networking software whose complexity is significantly beyond the scope of existing probabilistic verification tools.