Oxford logo
[Kwi13b] M. Kwiatkowska. Advances in Quantitative Verification for Ubiquitous Computing. In Proc. 11th International Colloquium on Theoretical Aspects of Computing (ICTAC 2013), volume 8049 of LNCS, pages 42-58, Springer, Heidelberg. 2013. [pdf] [bib]
Downloads:  pdf pdf (391 KB)  bib bib
Notes: The original publication is available at www.springerlink.com.
Abstract. Ubiquitous computing, where computers 'disappear' and instead sensor-enabled and software-controlled devices assist us in every-day tasks, has become an established trend. To ensure the safety and reliability of software embedded in these devices, rigorous model-based design methodologies are called for. Quantitative verification, a powerful technique for analysing system models against quantitative properties such as "the probability of a data packet being delivered within 1ms to a nearby Bluetooth device is at least 0.98", has proved useful by detecting and correcting flaws in a number of ubiquitous computing applications. In this paper, we focus on three key aspects of ubiquitous computing: autonomous behaviour, constrained resources and adaptiveness. We summarise recent advances of quantitative verification in relation to these aspects, illustrating each with a case study analysed using the probabilistic model checker PRISM. The paper concludes with an outline of future challenges that remain in this area.