www.prismmodelchecker.org

PRISM - Google Summer of Code 2016

We are delighted to announce that PRISM has been selected for the 2016 Google Summer of Code programme. This is a scheme where Google pays students (undergrad, MSc, PhD, ...) over the summer to get involved in Open Source projects. See their FAQ for details. We also previously participated in Google Summer of Code 2013 and 2014.

This page contains ideas for some potential PRISM-related projects that students might want to consider, and lists some of the mentors that have already signed up to guide students. We are also happy to hear your own ideas.

Interested?

  • Take a look at the projects below.
  • Play with PRISM a little. Download the source code, build it. You could also go from the svn repo too to get the very latest code.
  • Take a look at the first few parts of the online PRISM tutorial. Depending on the project you have in mind, you may not need a deep understanding of what PRISM does and how it works, but you should at least have a rough idea.
  • Discuss your project ideas (whether those below or their own) with PRISM's GSoC team. You can use the dedicated forum groups.google.com/group/prismmodelchecker-gsoc, which is specifically for PRISM-GSoC matters. Alternatively, you can email us at prismmodelchecker.gsoc@gmail.com, or contact one of the mentors directly (see the names attached to each project and the list at the bottom of this page).
  • Take a look at a list of simple bugs and feature additions that you can use to test that you got oriented in the code. You can include solution to these in your proposal to show your skills to us.

Applications

Applications can be made here starting 14 March 2016 at 19:00 (UTC) and ending 25 March 2016 at 19:00 (UTC).

You should use our template for applications.

Ideas

A full understanding of what PRISM does requires quite a lot of background (see here for some pointers), but this is not necessarily needed in order to contribute to the software. We have classified our project suggestions into 3 classes:

depending on the amount of background knowledge required.

Basic Projects

  • Enhanced graph plotting: PRISM includes JFreeChart to allow users to plot the results of their experiments graphically. But only a very limited range of graphs are supported. This project would extend this functionality, in particular providing support for: (i) histograms; (ii) error bars (to show numerical error, standard deviation etc.); (iii) 3-D surface plots (for experiments over multiple variables); (iv) better support for Pareto curves. For some aspects (e.g. 3D plotting), there is no support in JFreeChart, so the project would need to investigate additional open source libraries for graph plotting. [Possible mentors: VF, DP] [Languages: Java]
  • Web-based PRISM: This project will develop a web-based interface to PRISM (and, potentially to other probabilistic model checking software), allowing users to run the tool online without a local installation. An instance (or instances) of PRISM will run separately, either locally on the web-server or remotely, and communicate with the web application. The web interface will also act as tutorial with various simple models available pre-loaded. [Possible mentors: DP, LZ] [Languages: Web-based, e.g. JavaScript]
  • Server-client PRISM: PRISM's code base is already divided into a set of core "engines", which are shared between both the GUI and command-line versions of the tool. There is also a preliminary Java API for calling PRISM. This project will take these ideas further and develop a wrapper around PRISM that acts as a server/service to which external thin-clients can connect to run the tool. [Possible mentors: DP, BL] [Languages: Java]
  • Constraint solver backend interface: Some of the algorithms used by PRISM need constraint solvers (e.g. for linear programming). In most cases, the code does not allow the user to pick which solver to use, and adding a new solver requires a significant programming effort. This project will build on some recently added infrastructure to build a constraint solver backend interface that allows easy insertion and selection of new solvers. [Possible mentors: VF] [Languages: Java, C++]

Intermediate Projects

  • Property wizard and template language: PRISM uses temporal logic to allow the user to express system properties that should be verified. This project comprises two parts: (1) Create a "property wizard" for PRISM's GUI which will make it easier for users to create properties without needing to know the full details of the temporal logic syntax. (2) Design and implement a property template language to also simplify textual property specification for novice users. [Possible mentors: DP, GN] [Languages: Java]
  • Interactive tutorial: This project will develop an interactive, web-based tutorial to introduce new users to PRISM, perhaps based on some existing tutorial material. [Possible mentors: DP, JKl] [Languages: Web-based, e.g. JavaScript]
  • Graphical model editor: This project will develop a web-based user interface for drawing probabilistic models in a graphical fashion (similar to StateFlow). These graphical models will then be automatically translated to the standard textual PRISM modelling language and passed to the tool for verification or simulation. [Possible mentors: GN, DP] [Languages: Web-based, e.g. JavaScript]
  • Algorithm visualisation: PRISM relies on a variety of graph-based and numerical algorithms for the analysis of Markovian models. This project will create interactive visualisations of some of the core algorithms, possibly based on HTML and Javascript. Ideally, the visualisation will be automatically generated for a given, user-selected model by PRISM and tracks the actual computations in PRISM. [Possible mentors: JKl] [Languages: Web-based, e.g. JavaScript]
  • Constraint solving with custom constraints: Some of the algorithms used by PRISM internally convert a given model to a set of linear or non-linear constraints which are then solved by an external tool. Currently the constraints are created using Java code that needs to be written separately for every algorithm. This project will allow the user to input an XML file describing how constraints are created from a model. This will allow faster prototyping of new algorithms. [Possible mentors: VF] [Languages: Java, XML]
  • Refactoring and optimizing model construction for the explicit engine: PRISM's "explicit" engine does not use symbolic data structures for model construction and thus it provides an easier model manipulation that is beneficial for development of new functionality and methods within the PRISM framework. The goal of this project is to improve the scalability of the current model construction, implement efficient transformation of the explicit model into its sparse representation and provide full import/export of explicit models. [Possible mentors: MC, DP] [Languages: Java, C++]
  • Data-parallelization of core computational kernels: The majority of the core computational kernels in PRISM can be formulated as a series of matrix-vector operations. The goal of this project is to develop data-parallel OpenCL implementations of these kernels that will result in significant acceleration of the model-checking process on many-cores architectures. Recent research publications (see here and here) demonstrate the benefits of the GPU-acceleration of selected algorithms for quantitative analysis of probabilistic systems. [Possible mentors: MC] [Languages: Java, C++, OpenCL]

Advanced Projects

  • Exact solution methods : PRISM mostly uses floating point arithmetic and iterative numerical methods to compute probabilities, but in some instances it is preferable to use exact (arbitrary precision) arithmetic. This project will investigate the usage of (Java or C++) libraries for arbitrary precision arithmetic to support such calculations. An extension of this project could also consider building on this to implement the exact MDP verification techniques proposed in this paper. [Possible mentors: DP, SG, VF] [Languages: Java, C++]
  • Explicit-state model reductions: PRISM's explicit-state model checking engine now makes it much easier to implement model reduction techniques such as symmetry reduction, bisimulation minimisation, partial order reduction and others, which can be difficult to do well with the existing symbolic engines. This project will investigate implementation of these techniques. [Possible mentors: DP, GB] [Languages: Java]
  • Enhanced strategy functionality: On models such as Markov decision processes (MDPs) or stochastic games, PRISM works with strategies (also called adversaries, or policies): it can compute optimal strategies/adversaries and, in some cases, export them for external analysis. This project will enhance PRISM's support for strategies, allowing them to be explored in the simulator, re-imported from files or re-analysed using verification. [Possible mentors: DP, VF] [Languages: Java]
  • Compiler optimisations for PRISM models: The efficiency of model checking depends on many factors, but often small changes can made to the model, which do not affect its behaviour, yet improve performance. This project will implement automatic optimisation of PRISM language models with the goal of optimising model checking. [Possible mentors: DP, VF] [Languages: Java]
  • Efficient statistical model checking: PRISM has support for approximate/statistical model checking, which is based on discrete-event (Monte Carlo) simulation. The current engine works well, but is not optimised for speed and PRISM's guarded command based modelling language can be rather inefficient to simulate. This project will use compilation (to bytecode or a lower level language such as C) to improve the efficiency of statistical model checking, and consider other language-specific improvements to optimise simulation. [Possible mentors: VF, JKr] [Languages: Java]
  • Planning languages and techniques: One of the things PRISM can do is solve optimisation problems on Markov decision problems (MDPs). These are also widely used for planning problems, e.g. in the fields of robotics and AI. This project will implement connections between planning tools and languages (e.g. RDDL) other techniques for solving MDPs that may perform well (e.g. topological value iteration). [Possible mentors: BL, DP] [Languages: Java]
  • Probabilistic Boolean networks: Probabilistic Boolean networks (PBNs) are a well established computational framework for modelling biological systems. This project aims to build a translator from PBNs to PRISM, enabling PRISM for the analysis of biological systems modelled as PBNs. [Possible mentors: JP] [Languages: Java]
  • Extended support for mean-payoff properties: This project will add support for verification of multi-objective mean-payoff properties to PRISM. Recent research publications [CKK15, FKK15] have proposed new algorithms for verification of such properties, and the main task in this project is to implement these algorithms. [Possible mentors: VF, JKr] [Languages: Java]
  • Extended support for deterministic delays: PRISM users frequently want to incorporate deterministic (or, equivalently, fixed) delay events into CTMC models (see here). Recently, PRISM was experimentally extended with modelling support and some model checking functionality for fixed-delay CTMCs. This project will add steady-state analysis and the corresponding model checking options for an easy-to-solve class of fixed-delay CTMCs (see here). [Possible mentors: VR, LK] [Languages: Java]
  • Parallel Gauss-Seidel: The Gauss-Seidel method is an efficient way to perform probabilistic computation, such as value iteration. However, it is intrinsically sequential as it is very sensitive to the order of elements being processed. On the other hand, graphics cards have been popular in supercomputing for their parallel computation capability. This project will explore the possibility of developing a parallel version of Gauss-Seidel method using graphics cards. [Possible mentors: DP, HQ] [Languages: Java, C++]
  • Adaptive state space aggregation for Markov Models: This paper introduced an efficient adaptive state-space aggregation scheme for Markov chains describing biochemical reaction networks. The aggregation can considerably reduce the state space and thus speed up the verification process while providing reasonable formal bounds on the approximation error. The goal of this project is to extend the the aggregation scheme to support more general classes of Markov models and integrate the aggregation techniques into PRISM. [Possible mentors: MC] [Languages: Java, C++]

PRISM Mentors

Available mentors for PRISM's Google Summer of Code

About PRISM