Researcher in the Spotlight: Thomas Neele

Hi, my name is Thomas Neele and I’m a PhD candidate in the Formal Systems Analysis research group within the Department of Mathematics and Computer Science. Professor Jan Friso Groote is my supervisor.

The goal of my research is to improve scalability model checking, which is a technique for formal analysis of the behavior of software systems. We analyze abstract, formal models to reason about the discrete behavior of concurrent software. This is a challenging task due to the combinatorial explosion of the state of each component, leading to an exponential blow-up in the state-space size. The problem is even harder when considering systems that contain real-time behavior.
 

Based on parameterized Boolean equation systems 

My approach is based on the abstract encoding of model checking problems called parameterized Boolean equation systems (PBES). In this framework, we are attempting to develop transformations that simplify the problem and also new approaches to solving PBES. Part of the challenge in this research is to communicate our ideas to others: it is not easy to explain the abstract mathematics involved in our approach. Our ideas and tools should be accessible to users in industry, and it is currently not clear how to do that effectively. 
 

New algorithm 

We have developed a new algorithm to solve PBES that model an infinite state-space. The PBES framework is very suitable for applying abstraction techniques, which have allowed us to implement several optimizations that make the approach much more efficient. My research can be applied in high-tech companies that rely on software for mission-critical tasks. Bugs in this kind of software can be very costly, therefore it’s important to have high confidence in its correctness. Model checking can provide the necessary guarantees. With my research, I hope to eventually develop better software quality, which means safer and more reliable systems. Good examples are MRI scanners and self-driving vehicles.