Automated quantitative software verification with PRISM

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.