UbiVal: Fundamental Approaches to Validation of Ubiquitous Computing Applications and Infrastructures
Lead Research Organisation:
University of Birmingham
Department Name: School of Computer Science
Abstract
Mark Weiser's vision of ubiquitous computing, in which computers become transparently and seamlessly woven into the many activities of our daily lives, is slowly becoming a reality. Researchers have created prototype ubiquitous computing environments such as 'smart homes' that can automatically sense the presence of a resident in a particular room and change some aspect of the environment of the room such as turning on the lights, or 'smart museums' that can play recorded information about the museum artefact a visitor is standing in front of. There seem to be limitless possibilities for the kinds of environments and applications that can be developed for ubiquitous computing, yet the very nature of ubiquitous computing creates new and significant challenges for engineers who would like to build these environments and applications. Anybody who has ever used a computer has experienced the extreme frustration of using a software package that doesn't work the way it's supposed to, or that unceremoniously crashes in the middle of its operation, or that runs extremely slowly, or that transmits sensitive information such as credit card numbers over untrusted networks. For ubiquitous computing to achieve true transparent and seamless integration with its surroundings, it is important to prevent such mishaps, crashes, inefficiencies and insecurities from happening to the greatest extent possible. This project will define and implement a suite of sound, systematic methods that engineers can use to create correctly functioning, efficient and secure ubiquitous computing environments and applications. The research will be conducted and evaluated using the smart urban spaces and applications being developed in another ubiquitous computing project called Cityware.
Publications
Kwiatkowska M
(2009)
PRISM probabilistic model checking for performance and reliability analysis
in ACM SIGMETRICS Performance Evaluation Review
Kwiatkowska M
(2008)
Analysis of a gossip protocol in PRISM
in ACM SIGMETRICS Performance Evaluation Review
Kwiatkowska M
(2007)
Stochastic Model Checking
in Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07)
Kattenbelt M
(2010)
A game-based abstraction-refinement framework for Markov decision processes
in Formal Methods in System Design
Norman G
(2009)
Model Checking Probabilistic and Stochastic Extensions of the p-Calculus
in IEEE Transactions on Software Engineering
Liu Z
(2010)
A biologically inspired QoS routing algorithm for mobile ad hoc networks
in International Journal of Wireless and Mobile Computing
Bucur D
(2010)
Software verification for TinyOS
in IPSN
Bucur D
(2011)
On software verification for sensor nodes
in Journal of Systems and Software
Etessami K
(2008)
Multi-Objective Model Checking of Markov Decision Processes
in Logical Methods in Computer Science
Etessami K
(2007)
Multi-Objective Model Checking of Markov Decision Processes
in Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07)
Description | This project has defined and implemented a suite of sound, systematic methods that engineers can use to create correctly functioning, efficient and secure ubiquitous computing environments and applications. At Oxford and Birmingham, the research focused on formulating probabilistic model checking techniques for analysing performance and reliability of ubiquitous computing applications; designing a framework for simulation and verification of wireless network protocols, including multi-objective specifications; analysing network security, anonymity and access control protocols; and developing software verification techniques and tools for sensor networks. The research was conducted and evaluated using several significant case studies, e.g. the Zigbee protocol, for which a range of performance and energy measures were automatically calculated for a variety of scenarios to identify possible improvements the design. |
Exploitation Route | The project developed methods as well as software, available from: http://qav.cs.ox.ac.uk/projects/epsrc-ubival/ |
Sectors | Digital/Communication/Information Technologies (including Software) |
URL | http://qav.cs.ox.ac.uk/projects/epsrc-ubival/ |
Description | This project has defined and implemented a suite of sound, systematic methods that engineers can use to create correctly functioning, efficient and secure ubiquitous computing environments and applications. At Oxford and Birmingham, the research focused on formulating probabilistic model checking techniques for analysing performance and reliability of ubiquitous computing applications; designing a framework for simulation and verification of wireless network protocols, including multi-objective specifications; analysing network security, anonymity and access control protocols; and developing software verification techniques and tools for sensor networks. The research was conducted and evaluated using several significant case studies, e.g. the Zigbee protocol, for which a range of performance and energy measures were automatically calculated for a variety of scenarios to identify possible improvements the design. |
Sector | Digital/Communication/Information Technologies (including Software) |
Description | EPSRC |
Amount | £444,316 (GBP) |
Funding ID | EP/G02684X/1 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 09/2009 |
End | 04/2014 |
Description | EPSRC |
Amount | £444,316 (GBP) |
Funding ID | EP/G02684X/1 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 09/2009 |
End | 04/2014 |
Description | EPSRC |
Amount | £991,396 (GBP) |
Funding ID | EP/H005501/1 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 03/2010 |
End | 09/2015 |
Description | EPSRC |
Amount | £254,321 (GBP) |
Funding ID | EP/F013442/1 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 09/2007 |
End | 03/2009 |
Description | EPSRC |
Amount | £418,296 (GBP) |
Funding ID | EP/F033540/1 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 09/2008 |
End | 03/2013 |
Description | EPSRC |
Amount | £991,396 (GBP) |
Funding ID | EP/H005501/1 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 03/2010 |
End | 09/2015 |
Description | EPSRC |
Amount | £418,296 (GBP) |
Funding ID | EP/F033540/1 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 09/2008 |
End | 03/2013 |
Description | EPSRC |
Amount | £254,321 (GBP) |
Funding ID | EP/F013442/1 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 09/2007 |
End | 03/2009 |
Description | Technology Strategy Board |
Amount | £213,973 (GBP) |
Funding ID | TS/I002529/1 |
Organisation | Innovate UK |
Sector | Public |
Country | United Kingdom |
Start | 06/2011 |
End | 07/2014 |