EPSRC logo

Details of Grant 

EPSRC Reference: EP/D07956X/1
Title: Automated quantitative software verification with PRISM
Principal Investigator: Kwiatkowska, Professor MZ
Other Investigators:
Researcher Co-Investigators:
Project Partners:
BT Djinnisys Corp. QinetiQ
Department: School of Computer Science
Organisation: University of Birmingham
Scheme: Standard Research
Starts: 01 January 2007 Ends: 30 June 2007 Value (£): 583,565
EPSRC Research Topic Classifications:
Fundamentals of Computing Modelling & simul. of IT sys.
Software Engineering System on Chip
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:  
Summary on Grant Application Form
Large-scale distributed systems, such as the Internet, broadband wireless at home and mobile phone networks, raise many challenges for the design and engineering of the underlying infrastructure. Such systems crucially depend on robust and efficient communication and coordination protocols that ensure that the overall system is self-organising, timely and energy-efficient, possibly in the presence of unreliable network services and malicious or uncooperative agents. New protocols for distributed coordination are being introduced to manage the limited resources. They increasingly often rely on randomisation, which plays an important role in achieving de-centralisation, and resource awareness, for example adapting to the power level. The combination of randomness and nondeterminism that arises from the scheduling of distributed components introduces complex behaviours that may be difficult to reason about. Assuring correctness, dependability and quality of service of such distributed systems is thus a non-trivial task that necessitates a rigorous approach, and methods for quantitative evaluation of such systems against properties such as ``the probability of battery level dropping below minimum within 5 seconds is guaranteed to be below 0.01 in all critical situations'', are needed. Theoretical foundations of such quantitative analysis have been proposed, with some implemented in software tools and evaluated through case studies. However, no tools and techniques can directly address real programming languages endowed with features such as random choice and timing delays.This proposal is to further develop the foundations for reasoning about probabilistic systems to enable quantitative analysis of real programming languages. The research will involve extending the successful quantitative probabilistic model checker PRISM (www.cs.bham.ac.uk/~dxp/prism/) via predicate abstraction, and develop additional enhancements to the PRISM toolkit in collaboration with the extensive user community. The resulting techniques will also be relevant for other domains in which probabilistic model checking has proved successful, e.g. performance analysis, planning and systems biology.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.bham.ac.uk