Abstract. Ubiquitous computing is a vision of computing in which the computer disappears from view and becomes embedded in our environment, in the equipment we use, in our clothes, and even in our body. Everyday objects - called 'everyware' by Adam Greenfield - are now endowed with sensing, controlled by software, and often wirelessly connected and Internet-enabled. Our increasing dependence on ubiquitous computing creates an urgent need for modelling and verification technologies to support the design process, and hence improve the reliability and reduce production costs. At the same time, the challenges posed by ubiquitous computing are unique, deriving from the need to consider coordination of communities of 'everyware' and control physical processes such as drug delivery.

Model-based design and verification techniques have proved useful in supporting the design process by detecting and correcting flaws in a number of ubiquitous computing applications, but are limited by poor scalability, efficiency and range of scenarios that can be handled. In this paper we describe the objectives and initial progress of the research aimed at extending the capabilities of quantitative, probabilistic verification to challenging ubiquitous computing scenarios. The focus is on a advancing quantitative verification in new and previously unexplored directions, including game-based techniques, incorporation of continuous dynamics in addition to stochasticity, and online approaches. The research involves investigating the fundamentals of quantitative verification, development of algorithms and prototype implementations, and experimenting with case studies.