A roadmap to pervasive systems verification

Abstract

The complexity of pervasive systems arises from the many different aspects that such systems possess. A typical pervasive system may be autonomous, distributed, concurrent and context based, and may involve humans and robotic devices working together. If we wish to formally verify the behaviour of such systems, the formal methods for pervasive systems will surely also be complex. In this paper, we move towards being able to formally verify pervasive systems and outline our approach wherein we distinguish four distinct dimensions within pervasive system behaviour and utilize different, but appropriate, formal techniques for verifying each one.