Automated quantitative software verification with PRISM

Lead Research Organisation: University of Birmingham
Department Name: School of Computer Science

Abstract

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.

Publications

10 25 50

publication icon
Ciesinski F (2008) Model Checking Software

publication icon
Etessami K (2008) Multi-Objective Model Checking of Markov Decision Processes in Logical Methods in Computer Science

publication icon
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)

publication icon
Feng L (2010) Compositional Verification of Probabilistic Systems using Learning in Proc. 7th International Conference on Quantitative Evaluation of SysTems (QEST'10)

publication icon
Heath J (2008) Probabilistic model checking of complex biological pathways in Theoretical Computer Science

publication icon
Kattenbelt M (2010) A game-based abstraction-refinement framework for Markov decision processes in Formal Methods in System Design

publication icon
Kattenbelt M (2008) Game-Based Probabilistic Predicate Abstraction in PRISM in Proc. 6th Workshop on Quantitative Aspects of Programming Languages (QAPL'08)

publication icon
Kattenbelt Mark Alex (2010) Automated quantitative software verification

Related Projects

Project Reference Relationship Related To Start End Award Value
EP/D07956X/1 01/01/2007 30/06/2007 £583,565
EP/D07956X/2 Transfer EP/D07956X/1 01/07/2007 30/09/2010 £539,902
 
Description The project has developed several novel techniques for verification of quantitative properties of software and applied them, for the first time, to real programming languages such as C. An underlying theoretical framework was defined for constructing abstractions of systems that exhibit probabilistic and timed behaviour, automatically refining these abstractions and verifying quantitative properties such as performance, reliability and resource usage [KKNP10, KH09a, KNP10b, Kat11]. Efficient algorithms to implement this framework were developed, based on predicate abstraction and convex polyhedra (zones), and built into software tools for quantitative verification [KNP09c, KKNP09, Kat11]. This includes QProver a tool for verifying a probabilistic extension to ANSI C, applied to real source code for several network utilities, and a new version of the PRISM model checker, which allows probabilistic programs to be extended with real-time behaviour. The project has also developed several other techniques for improving the efficient of verifying probabilistic systems, including compositional (assume-guarantee) model checking [EKVY08, KNPQ10], algorithmic learning [FKP10] and symmetry reduction [DMP09]. These have been applied to the analysis of numerous large case studies, ranging from communication protocols to systems biology [HKN+08, KNP09b, KNP10a].

Citations are to publications listed here:
http://qav.comlab.ox.ac.uk/projects/epsrc-swverif/publications.php
Exploitation Route The project developed methods as well as software, available from:

http://qav.comlab.ox.ac.uk/projects/epsrc-swverif/
Sectors Digital/Communication/Information Technologies (including Software)

URL http://qav.comlab.ox.ac.uk/projects/epsrc-swverif/
 
Description PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. It has been used to analyse systems from many different application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, biological systems and many others. See http://www.prismmodelchecker.org/
Sector Digital/Communication/Information Technologies (including Software)
 
Description EPSRC
Amount £5,055,294 (GBP)
Funding ID EP/F001096/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 07/2007 
End 06/2013
 
Description EPSRC
Amount £5,055,294 (GBP)
Funding ID EP/F001096/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 07/2007 
End 06/2013