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
Dennis L
(2016)
Formal verification of ethical choices in autonomous systems
in Robotics and Autonomous Systems
Fisher M
(2009)
Executable specifications of resource-bounded agents
in Autonomous Agents and Multi-Agent Systems
Fisher M
(2011)
Agent deliberation in an executable temporal framework
in Journal of Applied Logic
Konur S
(2013)
Combined model checking for temporal, probabilistic, and real-time logics
in Theoretical Computer Science
Konur S
(2014)
A roadmap to pervasive systems verification
in The Knowledge Engineering Review
Konur S
(2012)
Analysing robot swarm behaviour via probabilistic model checking
in Robotics and Autonomous Systems
Konur S
(2014)
Formal verification of a pervasive messaging system
in Formal Aspects of Computing
Schewe S
(2009)
Büchi complementation made tight
Slavkovik M
(2014)
An abstract formal basis for digital crowds
in Distributed and Parallel Databases
Stocker R
(2012)
Logics in Artificial Intelligence
Stocker R
(2011)
Computational Logic in Multi-Agent Systems
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 | Public |
Country | United Kingdom |
Start | 01/2016 |
End | 12/2020 |