Formally verified, rapid prototyping for Air Traffic Control

The development of safety critical systems in areas such as Air Traffic Control (ATC) requires a range of disciplines. A focus on providing a usable and safe interface for controllers is vital. This paper presents a prototyping environment for creating complex, concurrent multi-user systems. It allows systems to be built in a high level, structured manner. With this environment, it is also possible to verify important safety properties about a prototype implementation. To make the verification practical we focus on critical areas of the design. This avoids the state-space explosion problems faced when trying to perform exhaustive proofs about a whole system. We demonstrate how this environment was used to produce a prototype data-link ATC system, for En-Route traffic, with co-operation from a UK ATC provider.