Skip to main content
University of Oxford Department of Computer Science
  Contact Us     Search  
  1. Home
  2. Our Students
  3. Online Resources & Handbooks
  4. Student projects - Quantitative/Probabilistic Modelling, Verification and Synthesis

Quantitative/Probabilistic Modelling, Verification and Synthesis

Supervisor

Personal photo - Marta Kwiatkowska Marta Kwiatkowska

Suitable for

Computer Science
MSc in Computer Science

Abstract

Professor Marta Kwiatkowska is happy to supervise projects in the area of quantitative/probabilistic modelling, verification and synthesis, particularly those relating to the PRISM model checker. PRISM is an open source formal verification tool for analysis of probabilistic systems. PRISM has an extensive website which includes software for download, tutorial, manual, publications and many case studies. Students' own proposals in the broad area of theory, algorithms and implementation techniques for software verification/synthesis will also be considered.

Below are some concrete project proposals:

  • Modelling trust in human-robot interaction. When human users interact with autonomous robots, appropriate notions of computational trust are needed to ensure that their interactions are safe and effective: too little trust can lead to user disengagement, and too much trust may cause damage. Trust management systems have been introduced for autonomous agents on the Internet, but need to be adapted to the setting of mobile robots, taking into account intermittent connectivity and uncertainty on sensor readings. Recently, a quantitative reputation-based trust model for user-centric networks has been modelled and analysed using PRISM-games, http://www.prismmodelchecker.org/games/ , an extension of the PRISM model checker which supports stochastic multi-player games as models and objectives expressed in temporal logic ( http://www.prismmodelchecker.org/bibitem.php?key=KPS13 ). This project aims to develop a quantitative trust management system that is suitable for mobile robots. Initially, a simplified setting will be considered and an approach to modelling trust developed for this setting. The project will suit a student interested in modelling and/or software implementation.

  • Autonomous urban driving. This project is concerned with synthesising strategies for autonomous driving directly from requirements expressed in temporal logic, so that they are correct by construction. Probability is used to quantify information about hazards, such as accidents hotspots. Inspired by the DARPA Urban Challenge, a method for synthesising strategies (controllers) from multi-objective requirements was developed and validated on map data for villages in Oxfordshire ( http://www.prismmodelchecker.org/bibitem.php?key=CKSW13 ). The idea is to develop the techniques further, to allow high-level navigation based on waypoints, and to develop strategies for avoiding threats, such as road blockage, at runtime. In the longer term, the goal is to validate the methods on realistic scenarios in collaboration with the Mobile Robotics Group. The project will suit a student interested in theory or software implementation. For more information about the project see http://www.veriware.org/autonomous.php

  • Controller synthesis for robot coordination. Autonomous robots have numerous applications in scenarios such as warehouse management, planetary exploration, or search and rescue. In view of environmental uncertainty, such scenarios are modelled using Markov decision processes. The goals (e.g. the goods should be delivered to location A while avoiding the hazardous location B) can be conveniently specified using temporal logic, from which correct-by-construction controllers (strategies) can be generated. This project aims to develop a PRISM model of a system of robots for a particular scenario so that safety and effectiveness of their cooperation is guaranteed. Techniques based on machine learning, and specifically real-time dynamic programming ( http://www.prismmodelchecker.org/papers/atva14.pdf ), will be utilised to generate controllers directly from temporal logic goals. This project will suit a student interested in machine learning and software implementation.

  • Driver modelling. Semi-autonomous driving is intended to improve safety, and involves, for example, taking control of the car from the driver if a collision is predicted. Probabilistic models of driver behaviour are needed in order to monitor whether the driver is attentive or distracted, and to predict if the manoeuvre, such as the driver swerving to the neighbouring lane, is safe. Recently, a driver model was developed and analysed using PRISM ( http://www.prismmodelchecker.org/bib-ext.php?search=driver ) and validated against data from the Carsim simulator. This project aims to extend this model in a number of ways, firstly, with more realistic threats, and, secondly, with active threats; the latter can be achieved using stochastic games and the PRISM-games model checker ( http://www.prismmodelchecker.org/games/ ). In the longer term, the goal is to validate the model with real traffic data in collaboration with the Mobile Robotics Group. This project will suit a student interested in modelling.

  • Heartbeat identification for smartphones. Today’s smartphones and fitness gadgets provide a variety of apps for health monitoring. Monitoring the heartbeat has also been proposed for use as a password, to ensure security and privacy, and this idea is currently being developed in e.g. the Nymi wristband. As part of ongoing research, techniques have been developed to analyse the ECG signal to facilitate personalisation of pacemaker devices, see http://www.veriware.org/bibitem.php?key=KMP14 . This project aims to implement the method proposed in the paper “Human Identification Using Heartbeat Interval Features and ECG Morphology”, Proceedings of Seventh International Conference on Bio-Inspired Computing: Theories and Applications (BIC-TA 2012), Springer, 2013. The implementation will be evaluated using a hardware testbed to be provided. The project will suit a student interested in embedded software. For more information about the pacemaker project see http://www.veriware.org/pacemaker.php.

  • Modelling and analysis of energy usage for RFID protocols. Radio frequency identification (RFID) is used for object identification with application to devices connected to the Internet of Things. RFID protocols can benefit from formal verification techniques, and particularly quantitative verification with which a number of cost measures can be analysed. Recently, a Markov model was developed for performance analysis (“Performance Analysis of RFID Protocols: CDMA Versus the Standard EPC Gen-2”, IEEE Transactions on Automation Science and Engineering, vol.11, no.4, pp.1250-1261, 2014). The idea is to develop a parametric PRISM model ( www.prismmodelchecker.org ) based on this Markov model and analyse its energy usage characteristics. The advantage of the parametric model is that it can be used to automatically determine optimal parameter values that guarantee that a given property is satisfied. The PRISM model of the ZigBee protocol ( http://www.prismmodelchecker.org/casestudies/zigbee.php ) may be useful for this purpose. This project would suit a student interested in probabilistic modelling and Internet of Things.

  • Automated protocol synthesis from requirements. Network protocols are sets of rules that define how information is exchanged between computers or agents on a network. Many communication protocols, to mention Bluetooth, can be modelled as timed automata or their extensions. Protocols typically have the same algorithmic structure but may differ in values of parameters, e.g. timing delays. This project aims to develop a method for synthesising protocols from requirements given in temporal logic so that they are correct by construction. The idea is to combine template-based synthesis (“Template-based Program Verification and Program Synthesis”, Journal on Software Tools for Technology Transfer, 2012) with parameter synthesis for timed automata developed and implemented recently ( http://www.veriware.org/bibitem.php?key=DKKM14 ). This way, the algorithmic structure will be given as a parametric template, and appropriate parameter values can be selected automatically to optimise a given quantitative requirement. This project would suit a student interested in theory and/or constraint solving.

  • Probabilistic model checking for cellular microcolonies. The gro language enables the programming, modelling, specifying and visually simulating the behaviour of cells in growing microcolonies of microorganisms ( http://depts.washington.edu/soslab/gro/index.html ).  gro has been used for teaching of synthetic biology.  Microcolonies develop through e.g. cell division and cell growth, and can be described in a simple guarded command language.  This project aims to extend the gro framework with probabilistic model checking by translating the language to the PRISM modelling language ( www.prismmodelchecker.org ) and extending the functionality to allow for model checking queries specified in probabilistic temporal logic. The project would suit a student interested in programming and synthetic biology.

  • Modelling and verification of DNA programs. DNA molecules can be used to perform complex logical computation. DNA computation differs from conventional digital computation and is sometimes referred to as ‘computing with soup’ http://www.economist.com/node/21548488 . Correct design of DNA devices is error-prone and the task is supported by tools such as the DNA Strand Displacement (DSD) programming language and simulator (http://research.microsoft.com/en-us/projects/dna/default.aspx) developed at Microsoft. The DSD tool enables the probabilistic model checking of DNA circuits and has been used to identify a flaw in a DNA transducer gate (see http://qav.comlab.ox.ac.uk/bibitem.php?key=LPC+12). The aim of this project is to model and analyse DNA implementation of logic inference proposed in “Autonomous Resolution Based on DNA Strand Displacement”, DNA Computing and Molecular Programming, LNCS 6937, 2011. The project will suit a student interested in modelling DNA programs using DSD and/or PRISM. For more information about the DNA computing project see http://www.veriware.org/dna.php.

Our Students

Back to Top