« Back to main Programme

Taming event-driven software via formal verification

Thomas Gibson-Robinson

Chief Technology Officer, Cocotec

Event-driven software can be found everywhere, from low-level drivers, to software that controls and coordinates complex subcomponents, and even in GUIs. Typically, event-driven software is characterised as consisting of a number of stateful components that communicate by sending messages to each other. Event-driven software is notoriously difficult to test. There are often many different sequences of events, and because the exact order of the events will affect the state of the system, it can be easy for bugs to lurk in obscure un-tested sequences of events. Even worse, reproducing these bugs can be difficult due to the need to reproduce the exact sequence of events that led to the issue.

Formal verification is one method of solving this: rather than writing tests to check each of the different possible sequences of events, automated formal verification could be used to verify that the software is correct no matter what sequence of events is observed. In this talk, we will look at what capabilities are required to ensure that this will be successful, including what it means for event-driven software to be correct, and how to ensure that the verification can scale to industrial-sized software projects.

About Thomas Gibson-Robinson

Tom Gibson-Robinson is the CTO of Cocotec, which is a spin-out of the University of Oxford specialising on using formal verification to improve software development. Tom has over a decade of experience in building high-performance formal verification tools. Combined with his passion for programming languages and building software, he is the driving force behind Cocotec’s innovation and tools. Tom completed his DPhil at the University of Oxford in 2013 on the theory of analysing layered security protocols. Prior to launching Cocotec, Tom was a Senior Researcher at the University of Oxford, where he specialised in algebras for expressing and reasoning about concurrent systems, as well as in model checking algorithms and tools. He is the main author of Coco, a language and tool for modelling and verifying event-driven software, and of the FDR4 model checker.

Sponsored by

AdaCore Capgemini Engineering

Supported by

AdaCore
Capgemini Engineering
Ansys
Harmonics
LDRA
RTI
Phixos
Rapita Systems Ltd
SDC Systems
Sysgo
Vector
Wind River
DDC-I
Harmonic Software Systems
TEKTowr
TrustInSoft
SafeCap