Verifying Interoperability Requirements in Pervasive Systems

Lead Research Organisation: University of Liverpool
Department Name: Computer Science

Abstract

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.

Publications

10 25 50
publication icon
Dennis L (2016) Formal verification of ethical choices in autonomous systems in Robotics and Autonomous Systems

publication icon
Fisher M (2011) Agent deliberation in an executable temporal framework in Journal of Applied Logic

publication icon
Fisher M (2009) Executable specifications of resource-bounded agents in Autonomous Agents and Multi-Agent Systems

publication icon
Konur S (2013) Combined model checking for temporal, probabilistic, and real-time logics in Theoretical Computer Science

publication icon
Konur S (2013) Formal verification of a pervasive messaging system in Formal Aspects of Computing

publication icon
Konur S (2014) A roadmap to pervasive systems verification in The Knowledge Engineering Review

publication icon
Konur S (2012) Analysing robot swarm behaviour via probabilistic model checking in Robotics and Autonomous Systems

publication icon
Slavkovik M (2014) An abstract formal basis for digital crowds in Distributed and Parallel Databases

 
Description Techniques for the formal analysis of pervasive systems, including communicating systems, human-system interaction, ethical aspects, and swarms.
Exploitation Route Use of techniques fro more general autonomous, sensor-rich systems.
Sectors Digital/Communication/Information Technologies (including Software)

URL http://cgi.csc.liv.ac.uk/VPS
 
Description As well as leading to new, larger, project proposals this work provides a foundational basis for the formalisation and verification of pervasive systems
First Year Of Impact 2010
Sector Digital/Communication/Information Technologies (including Software)
 
Description Programme Grant
Amount £4,183,694 (GBP)
Funding ID EP/N007565/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 01/2016 
End 12/2020