Research

My research interests lie in the intersection of formal software verification and safety-critical software, with a particular focus on applying formal methods to autonomous robotic systems. I am keen to do research work that also provides practical benefits, producing usable tools that support verification, development, and future research projects.

Academic Profiles

My publication records are available on the following sites.

Profiles:

Automated Aircraft Control Systems

My second pot-doc job was as Post-Doctoral Researcher at Maynooth University, Ireland. I was part of a team researching formal verification techniques for automated aircraft engine control systems, as part of the the Verification and Validation of Automated Systems’ Safety and Security (VALU3S) project. Having long told people that a good place to start with formal specification of a system is by looking at its requirements, my work on this project gave me a fantastic opportunity to do just that. A longer round-up of my work on this project can be found in a blog post I wrote.

Much of my work during this job centred on the requirements for the civilian aircraft engine controller that our industrial partner had given us. We captured the requirements in FRET (the Formal Requirements Elicitation Tool, written by a verification team at NASA) and did a lot of collaborative with the industrial partner to make sure that our formalisation of their requirements meant what they had intended the requirements to say. In this sense, I took a step into Requirements Engineering for the first time.

Seeing that the requirements contained a lot of repetitions, I was reminded of a module on Refactoring (improving the structure of a program without changing its behaviour) that I took during my undergraduate degree. I began investigating the idea of being able to reorganise the requirements in structured way to make them easier to maintain. This idea was eventually implemented in a fork of FRET that I called Mu-FRET, which added one refactoring. More are being added by Oisín Sheridan.

Autonomous Robots in Hazardous Environments

My first post-doc job was a a Research Assistant in the Department of Computer Science at the University of Liverpool (and later, the University of Manchester), working on one of the Robotics and AI Hubs. I wrote blog post that gives a detailed round-up of my work during this job.

Most of my work in this job was for the Robotics and AI in Nuclear (RAIN) Hub. Other colleagues were involved in the the hubs for offshore, and space, so some of my collaborative work crossed over to those domains too. These environments are remote and hazardous to humans, so robotic systems deployed there require a high level of autonomy and rigorous verification.

My work on this project began with an extensive survey paper, and then focussed on linking heterogeneous verification approaches applied across an autonomous software system, and runtime verification of an autonomous system’s behaviour. I also lead a collaboration with the UK’s Office for Nuclear Regulation on developing guidance for developers of autonomous systems that ensures their systems are amenable to robust verification and can provide useful assurance evidence.

During this job I also helped setup the research group (now network) website alongside Rafael Cardoso, and was ‘volunteered’ to setup and run a Twitter account for the group (now network). Most of the activities we did for these projects got tweeted about, and can be found under #HazardousHubs.

PhD Thesis

My research interests include formal modelling, model checking, safety-critical systems, and programming. My PhD relates to formalising Safety-Critical Java (SCJ) using the state-rich process algebra Circus, which combines elements of Z and CSP. I was supervised jointly by Professors Ana Cavalcanti and Andy Wellings at the University of York.

SCJ adopts a new programming paradigm for applications that must be certified. SCJ programs have a specific concurrent design and use region-based memory management (instead of garbage collection); specialised virtual machines are available to execute SCJ programs. It is organised into three compliance levels, of ascending complexity. My PhD focuses on the most complex compliance level, the programs of which are highly concurrent, potentially multi-processor, and make use of suspension and a variety of release patterns. My PhD provides the most complex compliance level of SCJ with its first semantics, enables further integration with other Circus semantics for SCJ, and provides automatic translation from SCJ to our model.

A copy of my PhD thesis can be found on the White Rose repository. The slides for my Thesis Seminar, which is a presentation of my entire thesis work given just before the final hand in, can be downloaded here