Formalising a CORE requirements model in the air traffic control domain

In 1985, a two-year project was set up to investigate the applicability of software fault tolerance techniques to air traffic control systems. The project focussed on the potential use of recovery blocks for the radar data processing functions of the London Air Traffic Control Centre (LATCC) at West Drayton. During the initial stages of this project, it was necessary to formulate a retrospective requirements model for LATCC, and the controlled requirements expression (CORE) method (G.P. Mullery, 1979) was selected for this purpose. In 1988, a three-year project was undertaken which was concerned with investigating how the SD-CORE method might be strengthened by the complementary use of formal specification techniques. The Vienna Development Method (VDM) was identified as the primary focus. It was, however, recognised at this stage that other formalisms should be investigated to complement VDM and, during the project, communicating sequential processes (CSP) (C.A.R. Hoare, 1985) was selected for this purpose. The authors address the work of this latter project. The bulk of this work has been concerned with exploring the way in which VDM could be used to describe formally a CORE requirements model and, in order to validate and refine this work, the requirements analysis for a short term conflict alert ATC function was performed using the combined CORE/VDM approach