Verifying Interoperability Requirements in Pervasive Systems
MediaWiki has been successfully installed.
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 post-doctoral researchers and three PhD students will be working on the project:
- Post-doctoral RA at Liverpool - Savas Konur
- Post-doctoral RA at Glasgow - Chris Unsworth
- Post-doctoral RA at Birmingham - Myrto Arapinis
- Research student at Liverpool - Richard Stocker
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.
- 1st meeting, University of Glasgow, 13 November 2008
- 2nd meeting, University of Birmingham, 26 February 2009
- 3rd meeting, University of Birmingham, 26 June 2009
- 4th meeting, University of Birmingham, 8 October 2009
- 5th meeting, University of Glasgow, January 2010
- Myrto Arapinis, Tom Chothia, Eike Ritter, Mark Ryan - Untraceability in the applied pi-calculus. In proceeding of the 1st International Workshop on RFID Security and Cryptography (RISC 2009). (Bibtex | Slides)
- Myrto Arapinis, Muffy Calder, Louise Denis, Michael Fisher, Philip Gray, Savas Konur, Alice Miller, Eike Ritter, Mark Ryan, Sven Schewe, Chris Unsworth, Rehana Yasmin - Towards the Veriﬁcation of Pervasive Systems. In proceedings of the Third International Workshop on Formal Methods for Interactive Systems (FMIS 2009). (Bibtex | Slides)
- Muffy Calder, Philip Gray, Chris Unsworth - Tightly coupled veriﬁcation of pervasive systems. In proceedings of the Third International Workshop on Formal Methods for Interactive Systems (FMIS 2009)
- Savas Konur - Real-time and Probabilistic Temporal Logics: An Overview
- Sven Schewe - Büchi Complementation Made Tight. Proc. STACS 2009.
- Rafael H. Bordini, Louise A. Dennis, Berndt Farwer, and Michael Fisher. Automated Verification of Multi-Agent Programs. In Proc. 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2008.