zbMATH — the first resource for mathematics

Advances in quantitative verification for ubiquitous computing. (English) Zbl 1405.68186
Liu, Zhiming (ed.) et al., Theoretical aspects of computing – ICTAC 2013. 10th international colloquium, Shanghai, China, September 4–6, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39717-2/pbk). Lecture Notes in Computer Science 8049, 42-58 (2013).
Summary: Ubiquitous computing, where computers ‘disappear’ and instead sensor-enabled and software-controlled devices assist us in everyday 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.
For the entire collection see [Zbl 1271.68048].
Reviewer: Reviewer (Berlin)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
Full Text: DOI