A railway barrier has one job: to be down before the train arrives, every time. It is one of many systems that must act within strict time limits, from air-traffic control to pacemakers, where a moment's delay can be dangerous.

During his PhD studies, Mikael Bisgaard Dahlsen-Jensen built a tool that works out how to keep such systems acting safely and on time. The right timing values are hard to pin down: some, like how long the barrier takes to lower, are unknown when the system is being designed, and others can never be known exactly, such as when a train reaches the crossing after a sensor trips. On top of that, no designer controls the environment. A driver may weave around a half-lowered barrier, and the system must cope regardless.

Instead of just guessing values and then testing them, his tool computes the answer, automatically working out all the values that are guaranteed safe. It treats the problem as a game, with that uncontrolled environment as a worst-case opponent, and finds a strategy that wins no matter what it does. All of this is built into established verification software, and the underlying method is mathematically proven correct, not just tested, so an engineer can trust its answers before a design is ever built.

This summary was prepared by the PhD student.