The Application of Z to the Specification of Air Traffic Control Systems: 1. An Initial Specification of the Radar Processing Activity
Abstract
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 Centre (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 are discussed and potential benefits for the Civil Aviation Authority are highlighted. Great Britain.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 1989
- Accession Number
- ADA212402
Entities
People
- L. N. Simcox
Organizations
- Royal Signals and Radar Establishment