Verifying Interoperability Requirements in Pervasive Systems

The success of pervasive computing depends crucially on the ability to build, maintain and augment interoperable systems: components from different manufacturers built at different times are required to interact to achieve the user's overall goals.Pervasive systems often contain devices which must operate in very different environments and connect together in different ways, e.g., over ad-hoc wireless connections to a variety of systems, and still satisfy all the desired security and performance properties. Our approach to verifying these properties is to identify interoperability requirements for the interaction between the devices and their environment. These requirements introduce also an important layer of abstraction because they allow modularity in the verification process: it suffices to show that each mobile device or fixed component meets the interoperability requirements, and that the interoperability requirements entail the desired high-level properties.We argue that this verification framework makes it possible to adapt and extend techniques (such as model checking and process algebras) which have traditionally been used for verifying properties of small homogeneous systems, to large heterogenous systems. To support this thesis, we will develop techniques to verify properties concerning important aspects of heterogenous systems' security, individual and collective behaviour, performance and privacy. We will use the formal techniques to verify the consequent interoperability requirements, and evaluate their effectiveness through case studies.Note that our focus is on the verification of designs; in particular we focus on the design of basic component behaviours and the protocols which dictate access to them and interaction between them. It is important to note our intention is not to develop pervasive computing systems as such, but rather to draw motivation from, and test our ideas in, a number of planned and existing systems.Three case studies are planned; two are with industrial collaborators. The case studies will be drawn from three layers typical within pervasive systems: application, infrastructure and network. One industrial case study will be a healthcare application. One of its crucial features is the need for the monitoring device to operate in different environments. Hence a careful analysis of the necessary interoperability requirements is mandatory for this application. We will develop and apply our techniques as the system is designed, thus influencing directly the design of the application, motivating our techniques as we develop them, and gaining real life experience of applying our techniques in the field. In addition, our past experience indicates that we will also bring in further case studies, as the project develops. Drawing on the variety of expertise of the members of the consortium, we hope to make a step change in verification technology by developing novel techniques and learning which techniques are most effective in different contexts. The outcomes will directly benefit system designers, and indirectly, end users. They will include techniques applicable to a wide range of application domains, and results and lessons learned from three specific applications including a healthcare data capture system and RFID system infrastructure.