Using Mathematical Logic to Make Computer Systems More Reliable

Having joined SnT in 2020, Joshua Dawes is a postdoctoral researcher in the Software Verification and Validation (SVV) research group. His research interests lie in the fundamental research necessary to analyse the behaviour of programs, and the engineering work necessary to apply program analysis in an industrial context. Today he shares with us details of his day-to-day research.

What is your area of research?

“The main area of my research involves, like many others in SVV, verifying that certain kinds of computer systems behave as intended. In particular, I focus on a kind of testing that aims to check whether a computer system is not only generating the correct answer, but is executing the correct sequence of steps to get there. The problem can be tricky enough on its own without additional factors that we need to check for – such as how data looks throughout this sequence of steps, and how long each step takes.

My work in this area began during my Ph.D., which I spent at the European Organisation for Nuclear Research (CERN) in Geneva. There, I mainly investigated ways to rigorously analyse the relationship between the data being processed by computer systems, and the time taken. For example, if data is sent over a network, and it needs to be written into a database somewhere, you’d often expect there to be a relationship between that data and the time taken to perform certain operations on it.

A key aspect of my Ph.D. research, and now my research at SnT, is the use of maths to perform analyses of computer systems’ behaviour. The main kind of maths I use is the area of logic. Like many others, I use this because it tends to be convenient to write statements that should be true or false when a computer system runs.

How does the everyday use of logic differ from the mathematical kind?

Usually, in everyday speech, logic is used in sentences like, "To solve this problem, we could employ logic." In mathematical logic, we often refer to a logic, and this is a very different kind from that which is used in everyday speech – so it’s often a source of confusion. Here’s some clarification: a logic, mathematically speaking, is a language in which we can write things that should be true or false (usually), with respect to some defined world. A well-known one is propositional logic, a language that lets us say simple things about the world, like, “That tree is pink.” Since there are many of these logics, we can refer to individual ones; as each one provides useful features for writing specific kinds of statements.

How does this apply to computer systems?

Since running computer systems generate sequences of snapshots, a good choice of logic to describe how a computer system should behave – i.e. what should be true about it when it runs – should allow us to talk about multiple snapshots at the same time. This is where temporal logics come in, which are a group of languages that allow us to write statements concerning multiple points in time. For example, in the famous linear-time temporal logic, we could assert that, “Whenever Josh takes a sip of tea, eventually his mood will improve.”

As part of my research, I’ve introduced new temporal logics that make writing statements about certain behaviours in computer systems easier than it should be. My focus at SnT is developing new temporal logics and further analysis methods. The goal is to make the lives easier for people who develop computer systems whose components are both software and hardware.

In general, I enjoy this area of research, because you need a solid mathematical foundation but also strong programming skills. There’s a nice mix of formal maths and application in the real world. This is especially good because, in my opinion, we’re not doing research for the sake of it – we’re doing it to build tools that will be useful to people who need to analyse important systems in the industry. Good thing I came to SnT, then!”