From software verification to 'everyware' verification

摘要

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 'every ware' 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 'every ware' and control physical processes such as drug delivery. Model-based design and verification techniques have pro-ved 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 algo- rithms and prototype implementations, and experimenting with case studies.