VERIWARE: From Software Verification to Everyware Verification

In the words of Adam Greenfield, “the age of ubiquitous computing is here: a computing without computers, where information processing has diffused into everyday life, and virtually disappeared from view”. Conventional hardware and software has evolved into ‘everyware’ – sensor-enabled electronic devices, virtually invisible and wirelessly connected – on which we increasingly often rely for everyday activities and access to services such as banking and healthcare. The key component of ‘everyware’ is software, embedded inside electronic gadgets and continuously interacting with its environment by means of sensors and actuators. Ubiquitous computing must deal with the challenges posed by the complex scenario of communities of ‘everyware’, in presence of environmental uncertainty and resource limitations, while at the same time aiming to meet high-level expectations of autonomous operation, predictability and robustness. This calls for the use of stochastic modelling, discrete and continuous dynamics, quantitative measures, and goal-driven approaches, which the emerging quantitative software verification is unable to address at present.

The central premise of the VERIWARE project is that there is a need for a paradigm shift in verification to enable ‘everyware’ verification, which can be achieved through a model-based approach that admits discrete and continuous dynamics, the replacement of offline methods with online techniques such as machine learning, and the use of game-theoretic and planning techniques. The project will significantly advance quantitative probabilistic verification in new and previously unexplored directions. This will involve investigating the fundamental principles of ‘everyware’ verification, development of algorithms and prototype implementations, and experimenting with case studies.