Case Study: Safety in the National Airspace System

The NASA NextGen project has a goal to double the number of planes in the sky, while remaining extremely safe: one error for every billion hours of flight time. Keeping airplanes apart at a safe distance is not as simple as it may sound; it requires a huge number and variety of different sorts of systems to act in concert: the pilots, air traffic control towers, different sorts of radars, collision avoidance systems, the jets and wings of the aircraft, etc. Each of these was designed independently of the others—the radar manufacturers and the collision avoidance system manufacturers did not consult each other, let alone the pilots—and yet when coordinated in just the right way, they work together to make a remarkably safe system. 

However, because of its enormous complexity, the safety of the system rested on not changing too much, whereas NextGen threatened to change everything. Researchers from Honeywell recognized this as an opportunity to involve category theory and reached out to David Spivak at MIT to help. With a multimillion dollar grant from the US government, they teamed up to find the mathematics with which to reason about the behavior of the NextGen system. They developed Temporal Type Theory, a new time-based logic of behaviors, in which each component could each announce its own contract of behavior, some based on sending and receiving signals, others based on physical laws of motion, still others on the inherent delay of pilot deliberation. The logic acts as a big tent in which to do the final safety analysis for such a system. 

Honeywell called this work a game-changer, saying we “changed the landscape”, and NASA’s Official Assessment of our work begins: “The quality of the research produced under this contract was very innovative and really changes the way one thinks about systems of systems.” It goes on: “The goal of the research to apply category theory to model aerospace systems-of-systems is truly thinking outside the box. These sorts of efforts often flounder due the fact that the mathematicians just want to do pure math and are not that interested in delving into the application domain while the aerospace folks lack the background in pure math and wind up using the tried and true methods they always use. This project was a success primarily due to the fact that the contractor did a superb job in constructing the right team. David Spivak at MIT may be the leading mathematician in the world at applying category theory modeling to engineering applications such as aerospace and controls. I do not think the project would have succeeded with anyone else.”

Topos follows this model: We work with scientists and engineers who know a given domain, using category theory to find solid mathematical connections between systems that need to work together, even if these systems are of very different natures.