Application of Z to the Specification of Air Traffic Control Systems: 1. An Initial Specification of the Radar Processing Activity.

摘要

This report describes an initial investigation into the formal specification language Z and its applicability to Air Traffic Control Systems. The software corresponding to the initial radar plot processing in the multi-radar automatic tracking system at the London Air Traffic Control Center (LATCC) was used in the investigation. An informal pseudo code description of the radar plot processing function was taken as the 'requirements' and converted into a formal specification in the Z language. The specification was partly validated using an RSRE Z syntax and type checking tool. The experience gained during the exercise is discussed and potential benefits for the Civil Aviation Authority are highlighted. Great Britain. (RH)