PRISM Model Checker

License: GNU General Public License version 2.0 (GPLv2)

Web Page: http://www.prismmodelchecker.org/gsoc/

Mailing List: https://groups.google.com/forum/?fromgroups#!forum/prismmodelchecker-gsoc

PRISM is a software tool for modelling and studying the behaviour of real-life systems whose behaviour exhibits unpredictability or randomness. It can be used to analyse everything from the reliability of distributed file systems, to the performance of a Bluetooth-enabled wireless device, to the safety of a car's airbag control system. PRISM has been used by researchers worldwide in fields as diverse as quantum cryptography, systems biology, computer security and robotics. Development of PRISM is based at the University of Birmingham and the University of Oxford, UK, but we have contributors worldwide. It has been under development for over 10 years and contains about 200K lines of code in total. The software is coded primarily in Java, including a graphical user interface written in Swing, but with various underlying libraries written in C/C++.

Projects

• A Prototypical PRISM Extension for POMDPs POMDPs provide a principled mathematical framework for planning and decision-making in uncertain and dynamic environment, which is essential for autonomous systems. PRISM hasn’t supported model checking for POMDPs yet. With some new efficient POMDP algorithms invented in recent years, it is possible to extend PRISM for POMDPs. In this project, I propose to develop a prototypical PRISM extension for POMDPs.
• Counterexamples for Discrete Time Markov Models This project will add support for counterexample generation for Discrete Time Markov Chains and Markov Decision Processes to PRISM. That is, during the course of the project, several algorithms will be implemented in PRISM that, given a probabilistic reachability property and a DTMC or an MDP that violates said property, generate a counterexample explaining to the user why the model does not satisfy the property.
• Enhanced discrete-event simulation This project includes several enhancements which will improve both manual path generation and the process of statistical model checking.
• Model visualization and exploration The aim of this project is to enhance user's experience with PRISM by allowing the user to view and interactively explore state graphs. I propose to use JGraphX (A Java Swing diagramming (graph visualization) library) and additionally GraphML (An XML based file format for realizing graphs) for the same. This would add more features to the existing PRISM framework and would also help in delivering a better working environment to the user.
• Parameter space exploration for computational systems biology In the context of computational systems biology, a question is how to identify parameters of a CTMC so that the model fits with actual biological experiments, for the particular parameter values cannot be usually inferred from the experimental data only. A related problem is the exploration of parameter values with respect to changes in the system dynamics. The aim of the project is to implement techniques of this kind and enhancements thereof as part of the PRISM model checker.
• Prism: GSoC'14 Proposal Enhanced Graph Plotting: Adding functionality to Prism for 3D surface plots, histograms, error bars to make it more interactive for the user.
• Qixia's proposal for parameter synthesis framework The steady-state distribution of a Markov chain is an important quantity to analyse the corresponding biological system. We focus on developing simulation-based methods to calculate the steady-state distribution of relatively large Markov chains, which can lead us to estimate the model’s parameters by fitting the calculated steady-state distribution with the experimental measurements. Simulation-based methods, e.g., perfect simulation, are expected to be programmed as a component of PRISM.
• Verification of PCTL Properties of MDPs with convex uncertainties in PRISM We plan to integrate within PRISM an algorithm for the verification of Probabilistic Computation Tree Logic (PCTL) properties of Markov Decision Processes (MDPs) whose state transition probabilities are only known to lie within convex uncertainty sets. We have recently presented the first-known polynomial time verification algorithm for PCTL properties of CMDPs. We now plan to integrate this algorithm within PRISM, and to demonstrate it with case studies.