Formal methods and air traffic control-opportunities and limitations

Formal methods technology has matured sufficiently in recent years for it to be applied cost effectively in systems development. Cost effectiveness however requires that the use of formal methods is well focused and controlled; that is, applied at the appropriate level, to the appropriate parts of the system. This may involve specifications to clarify a requirement early on, or extraction of verification conditions for program proof later. The greatest payback from the use of formal methods is likely to be achieved in the development of systems that are complex, critical, and for which definitive descriptions can be produced from established experience of the problem area. These descriptions can then be used as a basis for defining rules that constrain the behaviour of the developed system when deployed in its environment. ATC systems clearly exhibit some of the properties described above, and may therefore by considered an ideal vehicle for the application of formal methods. However, as a short example application illustrates, the inadequate or inappropriate use of formal methods can still lead to production of a system that fails to meet its requirements. The author therefore highlights the need for verification and validation techniques to ensure the correct system is specified