Verifying Interoperability Requirements in Pervasive Systems

[A Research Project Funded by EPSRC]
Verifying Interoperability Requirements in Pervasive Systems


The ''Verifying Interoperability Requirements in Pervasive Systems'' project is an EPSRC-funded collaboration between the Universities of Birmingham, Glasgow and Liverpool in the UK.



Three vacancies for post-doctoral researchers will be available here:




The project brings together qualitative techniques, including deductive methods, model checking, and abstraction methods, with quantitative techniques, including probabilistic and performance analysis, in order to tackle the problem of verifying pervasive systems.

In order to tackle the challenge of pervasive system verification, the project aims to leverage the power of established techniques, notably

model checking,
a logic-based approach to analysing properties of state-based systems. There has been work (some of which was carried out by the investigators) on extensions such as parametrised model checking, infinite state model checking and probabilistic model checking, and this will be developed further within the project.
deduction and abstraction,
two closely linked, approaches that can be used either to reduce the verification problem to a scale suitable for model checking, or to tackle the larger problem directly.
process calculi
allowing high level descriptions of interaction, communication and synchronisation in concurrent systems.

Within the overall aim of developing viable and appropriate techniques for verifying interoperability requirements in pervasive systems, the project will address the following research objectives:

  1. develop frameworks for modelling interoperability requirements in pervasive systems (specifically, interaction requirements, performance and security).
  2. develop verification techniques that are tailored to analysing the requirements in models of pervasive systems.
  3. evaluate the techniques on significant case studies in a realistic application domain of distributed systems.

Outputs Produced

None yet!

Project Details

Relevant Links

None yet!

↑ Back to top

About this document ...

This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.70)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -no_subdir -no_navigation -t 'Verifying Interoperability Requirements in Pervasive Systems' -split 1 -address vps08.tex

The translation was initiated by Michael Fisher on 2008-03-12