Formal methods in a real air traffic control project

The Civil Aviation Authority is introducing a major new development into the London Air Traffic Control Centre. The central control function (CCF) is based on changes to the sectorisation of airspace to improve traffic throughput by introducing the so-called `tunnels-in-the-sky´. In support of CCF a number of computerised systems are being upgraded and new ones introduced. One of the new systems is the CCF display information system (CDIS). CDIS is a distributed real-time system running on a network of dualled computers communicating over a dual token ring local area network (LAN). The authors describe the use of formal methods in the development of CDIS