"Automated quantitative software verification with PRISM" is an EPSRC-funded project (grant reference EP/D07956X/2), running from July 2007 - September 2010. The project is led by Marta Kwiatkowska at the University of Oxford.
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 via predicate abstraction, and develop additional enhancements to the PRISM toolkit in collaboration with the 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.
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].
Publications: Software: