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.
People |
ORCID iD |
| Marta Kwiatkowska (Principal Investigator) |
Publications
Chatzikokolakis K
(2009)
Foundations of Software Science and Computational Structures
Ciesinski F
(2008)
Model Checking Software
Donaldson A
(2007)
GRIP: Generic Representatives in PRISM
Donaldson A
(2009)
Language-Level Symmetry Reduction for Probabilistic Model Checking
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)
Feng L
(2010)
Compositional Verification of Probabilistic Systems using Learning
in Proc. 7th International Conference on Quantitative Evaluation of SysTems (QEST'10)
Heath J
(2008)
Probabilistic model checking of complex biological pathways
in Theoretical Computer Science
Kattenbelt M
(2008)
Game-Based Probabilistic Predicate Abstraction in PRISM
in Proc. 6th Workshop on Quantitative Aspects of Programming Languages (QAPL'08)
Kattenbelt M
(2010)
A game-based abstraction-refinement framework for Markov decision processes
in Formal Methods in System Design
Kattenbelt Mark Alex
(2010)
Automated quantitative software verification
Kwiatkowska M
(2009)
Probabilistic Mobile Ambients
in Theoretical Computer Science
Kwiatkowska M
(2011)
PRISM 4.0: Verification of Probabilistic Real-time Systems
in Proc. 23rd International Conference on Computer Aided Verification (CAV'11)
Kwiatkowska M
(2010)
Formal Modeling and Analysis of Timed Systems
Kwiatkowska M
(2009)
PRISM probabilistic model checking for performance and reliability analysis
in ACM SIGMETRICS Performance Evaluation Review
Kwiatkowska M
(2009)
Formal Modeling and Analysis of Timed Systems
Kwiatkowska M
(2010)
Advances and Challenges of Probabilistic Model Checking
in Proc. 48th Annual Allerton Conference on Communication, Control and Computing
Kwiatkowska M
(2009)
Algorithmic Bioprocesses
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)
Kwiatkowska M
(2008)
Modeling and Verification of Real-Time Systems - Formalisms and Software Tools
Kwiatkowska M
(2007)
Quantitative Verification: Models, Techniques and Tools
in Proc. 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE)
Kwiatkowska M
(2009)
On Quantitative Software Verification
in Proc. 16th International SPIN Workshop
Norman G
(2009)
Model Checking Probabilistic and Stochastic Extensions of the p-Calculus
in IEEE Transactions on Software Engineering
| 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 |