PhD Projects

• Specifying and using properties of Heterogeneous Systems Techniques for specifying and using properties of single domain systems have been studied extensively, and have been shown to be very useful in practical applications, for both software and hardware. Systems involving components that are naturally described in different domains are less well studied. Developing an appropriate frame work for specifying properties of components in divergent domains, translating properties between multiple domains, finding the right projections to give the essential information to be used by connected components and developing correctness models for such systems has both theoretical and practical interest. This research could be undertaken in a number of different ways, ranging from pure theory through to very pragmatic studies showing results with significant examples, depending on the interest of the student(s).
• Cooperating proof tools for Heterogeneous systems There has been much research on, and great success in applying, automatic proof tools such as model checkers. More recently, the use of SAT solvers has shown to be a very useful enhancement of these tools. The extension of SAT into richer underlying domains with the use of SMT (Satisfiability modulo theory) is currently an active area of research. One of the properties of a heterogeneous system is that there is no single domain of reasoning that is ideal for all components. Extending the idea of SMT to allow multiple different theories to be supported would be a significant contribution to tools support for reasoning about such systems. This work could be undertaken at the theory level, the tool building level or the application level, depending on the background and interests of the student(s).

Verification of Security Hardware with Specification Obfuscation

Kevin Jones

Hardware verification, using both testing and formal approaches, is a well established and on-going area of EE/CS research. New approaches to security have resulted in classesof hardware that are difficult to verify using standard approaches. An interesting area of research, either for a EE interested in verification and proof or for a CS with an interest in hardware, is to develop and analyse techniques for verifying devices/IP blocks that serve a security function which requires some parts of the specification to be obfuscated. There is industrial interest in this problem and a high likelihood that a student undertaking this research would have collaborative contact with industrial design teams.

Lorenzo Strigini

When computers advise people in their decisions, paradoxical "over-reliance" situations may arise in which the computer's help makes people more likely to make mistakes rather than less likely. Theses are available to study by experiment and mathematical modelling how these situations arise, so that designers of systems from medical diagnosis aids to collision-alert systems for vehicles can forecast these situations and avoid creating them. This is an interdisciplinary topic straddling computing and psychology. To learn more about the open research questions, you may be interested in this paper and in our previous work on a medical application>.

Lorenzo Strigini

When computer based systems have critical functions, it is natural to test how well they would resist internal faults, accidental misuse or deliberate attacks, by artificially causing these kinds of stress. Many techniques in current use in  dependability and security apply this approach: for instance, fault injection, robustness testing, fuzzing, red teaming, penetration testing, mutation testing, dependability benchmarking. But how much should one be reassured if these tests are passed successfully? How difficult is it to create the "right" stresses? These questions require a mix of mathematical and empirical work. If interested in these issues, you may wish to look at discussions of open research questions for instance in this paper about software robustness or this paper about resilience of complex systems

Theses in these areas can aim at assessing by experiment the real predictive accuracy of these forms of measurement in specific applications (e.g. software security or robustness to error) and to prove by formal mathematical treatment what conclusions about a specific system can be drawn from these kinds of measurement.

Combination of formal proof with statistical testing of software

Lorenzo Strigini

Formal verification and statistical testing are two approaches to achieving confidence that software will perform as required.  However, for most complex systems neither method, alone, is sufficient. Confidence from proofs is limited by complexity of real-life requirements and of implementations, and of the proofs themselves; confidence from statistical testing depends on assumptions about the system being tested and the test process, which must be verified.

At the Centre for Software Reliability we have contributed to the state of the art in both these areas and have experience of their limits in concrete applications with critical software.  We are keen to supervise theses that will produce progress in combining the two categories of methods so that they support each other.

Effectiveness of alerting systems for security

Lorenzo Strigini

There is a booming business in developing advanced computer-based systems that help security and police forces to recognise criminals or dangerous situations and prompt intervention. These systems automatically analyse inputs from security cameras or other sensors and alert staff to consider reacting. Systems designed on similar principles alert computer system administrators to cyber intrusion. Designing these systems presents fascinating technical challenges, but the trickiest ones may be the socio-technical challenges, involving how the users react to these systems.  What is the risk of the computer causing false arrests or massive defence operations by false alarms? Or of it flagging a real danger but being ignored? These depend not only on how "clever" the computer is but also on how well it is matched to the abilities and decision making heuristics of the people using it.

This topic, related to our work on automation bias, requires interdisciplinary work at the intersection of system and software engineering with psychology, with possible interesting explorations of legal and organisational aspects, and may suit people with various backgrounds in hard sciences, computing or psychology.

Simone Stumpf

Sites such as Amazon, last.fm, etc offer recommendations of books, songs, etc based on the user's preferences. Previous research has focused on explanations of why recommendations are given, how to recommend items, as well as how users react to recommendations. This research will investigate approaches to recommendations and their effects from the perspective of the end-user.

Simone Stumpf

Previous research in Information Foraging Theory has concentrated on textual "scent" as part of the information seeking behavior of users. This research will explore information scent for images.

Simone Stumpf

This topic will investigate how risk assessment, information processing/seeking and interactions with systems may differ between gender or other user groups (such as people with high-functioning autism or Asperger's Syndrome) and how to support them better.

Neil Maiden

Many complex work tasks, both individual group, increasingly need creative thinking to be undertaken effectively. However, there is little tool support for creative thinking in work, in spite of the large numbers of creativity techniques available. New and innovative doctoral research is needed to explore the roles, features and interactions for new generations of creativity support tools embedded in work situations from healthcare to software design. The doctoral research will develop a new model of creativity and creativity support, then prototype and evaluate new types of software-based tools designed to support this creative thinking. The research will build on existing doctoral research in this direction.

Peter Weller

This project is concerned with providing real time information on seriously ill patients to mobile clinicians. The demands on clinicians are considerable especially for those involved in the care of patients in the high dependency environment. Frequently these clinicians have to attend to other tasks, such as ward rounds and case meetings, so immediate contact with patients in their care is lost. Currently pagers and phone conversations are used for staff to contact the clinicians should the condition of a patient deteriorate, but these can be ineffective and only provide information via another person so can be subjective or vague. The project will investigate the use of mobile and web technologies to research, implement and evaluate a mobile telemonitoring solution for clinicians. This problem domain is different to more traditional telemonitoring both in terms of the mobility of the monitored person and the demands of the clinical environment.

Peter Weller

The modern clinical environment is data rich with a large amount of data being routinely collected for most patient episodes. However, the full potential of these data to contribute to patient care are not always realised. Frequently, analysis or processing of the collected information can offer additional insight into patient condition and so provide the clinician with more knowledge for deciding on treatment. This can be especially useful for difficult to assess conditions, for example the level of sedation during surgery. This project is concerned with using a range of techniques from the artificial intelligence, mathematical modelling and statistical domains to analyse patient related datasets and hence to provide tools to support clinicians. Depending on the specific problem being addressed the student may be involved in data collection.

Tools for monitoring quality of patient care    

Peter Weller and Krish Thiru (Senior Public Health Specialist, London Specialised Commissioning Group)

Patients receiving NHS care are often not adequately followed up and given the best possible aftercare. This results in them often being readmitted and costing more to the NHS. The NHS now warehouses vast quantities of routine clinical and administrative data which is both structured (coded) and unstructured (textual) . Much of this data is focused on the individual patient and their clinical needs and is context specific (i.e  limited to one service or organisation) . The quality directives and the principles of implementing and monitoring of standards of care however require the NHS to identify, treat and follow up populations of patients over time, at the regional and national level. This is particularly relevant to chronic disease management (i.e. diabetic or coronary heart disease patients) but is just as applicable to specialised services (Long term ventilation patients, genetic conditions).
To manage populations of patients it is a prerequisite to be able to identify patient groups accurately. Often this cannot be effectively done by searching for specific codes or groups of codes or words within the sea of data. Probabilistic modelling (i.e Bayesian and regressional) can help to identify and establish 'virtual registers' of patents who are identified through constellations of codes and words, who can then be followed up over time.
This proposal aims to establish tools for the identification of group of patients for monitoring of quality of care using data from either the Hospital Episodic Statistics (HES) dataset and/or General Practice Research Database (GPRD). Such tools are essential to adequately use the yet untapped datasets available. This work can be conducted with anonymous data and therefore sits comfortably with the recent drive by the Government to make NHS data more easily available for research.
The reader is directed to:
http://www.reuters.com/article/2011/12/05/us-uk-reforms-idUSTRE7B419W20111205
http://www.bmj.com/rapid-response/2011/10/29/time-move-diagnostic-codes-disease-complexes

Ayse Goker

The drive in this topic area is: an interest to research, and improve information access and retrieval for users. Thus, the approach is to study information environments, investigate and develop novel techniques for enabling systems to be more effective in satisfying users information needs. These techniques can be described as learning algorithms, adaptive techniques, and personalisation approaches that consider the importance of the context or situation of the user. Work is then followed through with user-centred evaluation and the empirical data is then used to feedback into the system.

Different information environments have been researched within Web search and also the mobile environment. There is potential to extend on these or indeed to consider other ones. The importance of a user's context in these environments whether it is to do with topic, task, location, time or other aspect is critical. Different media also have different patterns of use.

For example, image storage/retrieval contexts can vary considerably depending on user context. The work would involve researching a focused aspect of any of the above in line with an applicant's background and research interests.

Andrew MacFarlane

Apart from research into blind and partially sighted users, there has been very little work on the problems disabled people have in accessing information either through navigation or directed search. There is plenty of scope for prospective candidates to choose an area of disabilities in which to conduct research, and there is a clear need for such work to help with social inclusion in information access systems. There are many different disabilities ranging from physical (blindness, cerebral palsy, quadriplegia etc.) to cognitive (dyslexia, dyspraxia, brain damage etc.), and I am interested in supervising projects which tackle any of these issues, particularly dyslexia (an area I am currently active in).

Andrew MacFarlane

An area of increasing interest in the world of search is understanding the needs of users for music and designing retrieval systems in the light of that information in order to satisfy the users needs. This is being driven by an increasing level of access to music for the general public via systems such as iTunes and the needs of professional music searchers such as music synchronisation workers who act as intermediaries between producers of music (Sony, BMG etc.) and consumers (advertising agencies, film and television companies, computer games software companies etc.). I am interested in supervising students who wish to conduct research into the needs of any type of user, and those who wish to build a music search system and test it using appropriate evaluation methodologies.

Library and Information Science

Lyn Robinson

Lyn is interested in working with potential  research students to develop studies in any of these areas: history and philosophy of information and documents; history of science, and its relation to the development of information resources; models and theories of information communication; domain studies, especially in science and healthcare; collections, and their changing nature; and the relations between the information sciences and the liberal arts.

Eduardo Alonso

It is paramount that we develop accurate, quick, user-friendly simulators of psychological models of learning and behaviour --to test their predictions.  For instance, in collaboration with experimental psychologists I have built the Rescorla and  Wagner Simulator (http://www.cal-r.org/index.php?id=software). We plan to develop software that would include additional features including attention, configural representations and real-time --features that are core in understanding clinical conditions. In so doing, we will be able to establish the explanatory power of the underlying psychological theories --thus facilitating their application in the treatment of pathologies and addictions.
Requirements: Good programming skills (preferably Java/C++; MATLAB) and  expertise in two of the following areas: neuroscience (learning and behaviour), machine learning (typically but not limit to neural networks), control and optimisation, dynamic systems. Applicants would also need to have a strong mathematical background

Eduardo Alonso

I am interesting in developing innovative Reinforcement Learning and Adaptive Dynamic Programming algorithms that would work in complex control systems. In such systems (be it a power plant or a supply chain for instance), engineers work with inherent uncertainty and thus need learning tools to dynamically calculate how to get to optimal and stable solutions. In the past we have developed a method that under certain conditions converges to (local) optimality --based on learning value-gradients over (imperfect) models. It works well in toy domains. We want to explore how such techniques (or similar techniques) would scale to real-life systems under different assumptions and constraints.
Requirements: Good programming skills (preferably Java/C++; MATLAB) and
expertise in two of the following areas: neuroscience (learning and
behaviour), machine learning (typically but not limit to neural networks),
control and optimisation, dynamic systems. Applicants would also need to
have a strong mathematical background

Formal models of evolution and learning

Eduardo Alonso

I am interested in exploring variational principles in learning and behaviour --using calculus of variations and abstract algebra. Such methods have been proved useful in expressing extremal principles that reflect constitutive and conservation laws as well as underlying symmetries in Nature. We plan to apply such methods to evolution and psychology.
Requirements: Good programming skills (preferably Java/C++; MATLAB) and
expertise in two of the following areas: neuroscience (learning and
behaviour), machine learning (typically but not limit to neural networks),
control and optimisation, dynamic systems. Applicants would also need to
have a strong mathematical background

Chris Child

Monte-Carlo based techniques have been shown to be effective in solving problems with large state-spaces. In recent years, research in the area has gained momentum, with a Monte-Carlo based GO player beating professional players for the first time. The techniques have also been applied successfully to Poker and Scrabble. These games present particular challenges to classical AI techniques, requiring extensive domain knowledge, or exponential time to generate effective behaviour due to large state spaces and stochastic world models. An issue with all Monte-Carlo based techniques is that they require either a world model or the ability to run a fast world simulation in order to form an effective policy. The research will develop techniques for modelling the world through experience, and using this world model for the Monte-Carlo learning stage. Possible world modelling techniques include: Two-Tier Bayesian Networks, Probabilistic Relational Planning Operators, or Parallel Stochastic Planning Operators.

Chris Child

Approximate Dynamic Programming (ADP) integrates techniques from dynamic programming (including reinforcement learning), mathematical programming, simulation and statistics. ADP techniques find an optimal mapping from state to action with respect to a reward function. Each field has developed methods in parallel for solving the three curses of dimensionality (i) the state space is exponential to the number of state variables (ii) the outcome space is exponential to the number of outcome variables (iii) the outcome-action space is exponential to the decision vector. Robust ADP solutions have been found for a range of problems areas in engineering, economics, operations research and artificial intelligence. Each of these solutions requires expert domain knowledge to for basis-functions, essentially extracting the state-variables relevant to the reward-function. This research will investigate methods for extracting planning rules that describe the problem domain, and using these to form basis functions for ADP techniques, thus alleviating the need for expert domain knowledge and facilitating the application of ADP techniques to a wide range of problem areas.

SAT Solving in Static Program Analysis

Jacob Howe

Static program analyses based on abstract interpretation require an abstract domain. One popular domain is that of polyhedra, and subclasses thereof, where relational information is expressed as linear inequalities. Whilst these domains have had successes, they are still limited by the computational cost of manipulating them, particularly when disjunctive information is required.

Much amount of effort has been put into the development of algorithms and tools for SAT (and SMT) solving and the result of this effort is a collection of very powerful solvers which have proved successful in many areas.

The use of the quadtrees datastructure has recently been proposed as an alternative abstract domain to polyhedra in static analysis.  This abstract domain allows many operations to be performed by SAT solvers, and allows a more natural treatment of disjunctive information.

The project could could be developed in the direction of mathematical or logic or in the direction of code analysis for safety and security vulnerabilities.  A major objective is to develop the theory of using SAT and SMT techniques in static analysis, whilst another is to develop tooling to exploit this theory.

Geometry for Static Analysis with Security Applications

Jacob Howe

The development of secure and safe software is strengthened by a final step of verification, in the sense of formally establishing that a precisely specified class of bugs does not occur. Recent work in program analysis has begun to achieve this.  However, success has been labour intensive since the framework needs to be refined for specific applications.

Analyses for buffer overruns use systems of inequalities known as polyhedra.  However, the operations in polyhedral analysis are computationally expensive. This has led to recent interest in subclasses of polyhedra that restrict the dependencies expressible in order to gain analyses that scale.

This project could be developed in a number of ways: working on computational geometry to further develop fundamental algorithms, working on tooling based on recent developments such as Logahedra, or more widely by working on constraint solving techniques.

Christos Kloukinas

The goal of this research is to develop a new software architecture language for describing complex software systems. This language is to be based on the "Components & Connectors" software architectural view but unlike other languages that have been developed so far, its focus will be on the connectors instead of the components. Connectors are the design elements that represent interaction protocols. Apart from describing a system, the language and associated tools should be able to analyse it for at least one non-functional property, e.g., reliability, availability, timeliness, etc.

Some initial ideas have been described in my article "Better Abstractions for Reusable Components & Architectures".

Christos Kloukinas

The goal of this research is to develop a formal model for a multi-processor real-time system that will allow us to automatically produce scheduling rules for its tasks.

The approach for producing such scheduling rules for a uni-processor system is described in my articles "Synthesis of Safe, QoS Extendible, Application Specific Schedulers for Heterogeneous Real-Time Systems", "A methodology and tool support for generating scheduled native code for real-time Java applications", and "Thunderstriking Constraints with Jupiter". It uses a series of model refinements and control synthesis to derive scheduling rules for different properties of a system.

Christos Kloukinas

The goal of this research is to develop a formal model for embedded systems that will allow us to automatically produce scheduling rules for its tasks so as to optimise its memory or power consumption.

The approach for producing such scheduling rules for deadlock-freedom and timeliness-related constraints is described in my articles "Synthesis of Safe, QoS Extendible, Application Specific Schedulers for Heterogeneous Real-Time Systems", "A methodology and tool support for generating scheduled native code for real-time Java applications", and "Thunderstriking Constraints with Jupiter". It uses a series of model refinements and control synthesis to derive scheduling rules for different properties of a system.

Christos Kloukinas

There is a way to automatically produce scheduling rules for a real-time system, that can guarantee it is deadlock-free and never misses a deadline (among other properties). This is described in my articles "Synthesis of Safe, QoS Extendible, Application Specific Schedulers for Heterogeneous Real-Time Systems", "A methodology and tool support for generating scheduled native code for real-time Java applications", and "Thunderstriking Constraints with Jupiter". It effectively uses a series of model refinements and control synthesis to derive the scheduling rules needed for the different properties of a system.

The problem with these is that they are extremely difficult to understand and, as such, to validate or optimise. For that reason we could try applying techniques from Machine Learning to better structure the scheduling rules, simplify them, and possibly even discover new ones. An initial step towards that direction is described in my paper "Data-Mining Synthesised Schedulers for Hard Real-Time Systems".

Automatic coronary artery stenosis detection and quantification

Greg Slabaugh

Coronary artery disease is the leading cause of death worldwide and typically results from the accumulation of plaques that narrow or obstruct blood vessels that supply blood and oxygen to the heart.  Computed tomography angiography (CTA) is a medical exam used to study blood vessels based on CT imaging and has advantages over other exams as it is less invasive.  The purpose of this project is to develop novel algorithms to automatically detect stenoses (narrowings of a blood vessel) in the coronary arteries and quantify / grade suspected areas from healthy to diseased, based on CTA imaging.  The intent is develop novel tools to help radiologists with detection and quantification to improve patient outcomes.

Peter Smith

Some recent work has determined that authorship attribution can be improved by a change in the distance metric used in the standard model (Smith and Aldridge, see also Burrows 2001). However the standard model assumes normally distributed data, which is incorrect. What is required is to create a model using alternate statistical distributions, e.g. negative hyper-geometric.

Peter Smith

There is still considerable work that can be done on the Shakespeare apocrypha for authorship attribution.

Peter Smith

Topics relating to the automation of sentiment analysis and mining text on the web -- for example automatic detection of news items and their impact on financial markets.

The Implications of Digital Technology on Social and Political Movements and their impact on Enterprises

David Chan

Manuel Castells talks of the network society and is currently monitoring the effects of social movements in the Arab Spring, the Occupy Wall Street Campaign etc. Governments are also taking action in the digital domain to counter these movements: some erecting firewalls like the People's Republic of China and others like Syria, purchasing scanning technologies to track activists.
I would like a PhD student to research:-
•    How current technologies are fuelling the changes in the power of social and political movements
•    Examine critically theories that account for the changes in behaviour of both movements and governments
•    Identify trends in technologies that are likely to be significant in the next decade (mobile connectivity, web 3.0, Large Data etc.) to the evolution of social and political movements
•    Explore their likely impact on socio-political movements and the business landscape
•    Identify future opportunities and future risks to enterprises
•    Propose strategies for enterprises in the new milieu
 This is an interdisciplinary research project involving an understanding of social and political sciences, computer sciences and business.

The Effectiveness of Certifications, Methodologies and Frameworks and their implications for Enterprises

David Chan

The IT industry has been subjected to a series of panaceas all purporting to be the answer to IT effectiveness within enterprises. Examples would include Business Process Re-engineering, Service Oriented Architectures, Enterprise Architecture, IT Enabled Change, Project Management, Web 3.0 etc. Dr Martin Rich already has a PhD student researching the effectiveness of different aspects of project management on the success of projects on enterprises. The industry has also adopted certification schemes such as TOGAF, Six Sigma, Prince 2, ITIL, MoR without any significant evidence base that these certification schemes have a positive impact on effective use of IT and IM.
I would like a PhD student to:-
•    Identify a number of IT certification schemes that are significant now and likely to be significant in the next decade
•    Undertake research to demonstrate their effectiveness or otherwise in enterprises through analysing real-world examples of their implementation
•    Review the literature and evaluate the appropriate paradigms and frameworks to position this analysis (Kurtz and Snowden. The Marshall Model, Intelligent Exploiter etc.)
•    Develop recommendations on what certification schemes should be supported by the industry and how these should be operated.