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:
- Birmingham;
- Glasgow;
- Liverpool
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:
- develop frameworks for modelling interoperability requirements
in pervasive systems (specifically, interaction requirements,
performance and security).
- develop verification techniques that are tailored to analysing
the requirements in models of pervasive systems.
- evaluate the techniques on significant case studies in a
realistic application domain of distributed systems.
- None yet!
- Project duration: 48 months
- Expected start date: Summer 2008
- EPSRC grant references
- None yet!
↑ Back to top
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 M.Fisher@csc.liv.ac.uk vps08.tex
The translation was initiated by Michael Fisher on 2008-03-12
M.Fisher@csc.liv.ac.uk