This module contains basic definitions of data that are the building blocks of the flight planning messages. The definitions are of a general nature and are applicable beyond the narrow focus of flight plan processing.
These definitions are required in support of the flight planning specification, but it is sufficient to skim this module to understand the remainder of the specification.
import LeanSpec.lib.Util
import LeanSpec.lib.Geo
namespace CoreA number of message fields are free text. While there is a restricted subset of ASCII characters allowed in the fields, for the purposes of this specification we will ignore such limitations.
def maxTextLength := 200
def FreeText := Str 1 maxTextLength
deriving DecidableEqDefinitions that relate to the flight that is the subject of a message.
The identifier used by air traffic control to identify the flight.
def AircraftIdentification := Str 2 7
deriving DecidableEqThe SSR (Secondary Surveillance Radar) is a code of four octal characters that is used to communicate with and track the flight. It is typically allocated by air traffic control shortly before take off.
def SsrCode := Str 4 4
deriving DecidableEqDepending on the level of equipment held, a flight can operate under instrument flight rules or visual flight rules.
inductive FlightRule
| ifr -- instrument flight rules
| vfr -- visual flight rules
deriving DecidableEqThe operating rules for the duration of a flight can be IFR, or VFR, or they may change during the flight.
inductive FlightRules
| i -- IFR
| v -- VFR
| y -- IFR first, but changing during flight
| z -- VFR first, but changing during flight
deriving DecidableEqFlights are categorised to assist with handling.
inductive TypeOfFlight
| s -- Scheduled flight
| n -- Non-scheduled flight
| g -- General Aviation (GA)
| m -- Military
| x -- Other
deriving DecidableEqSome flights receive special handling by air traffic control due to their nature. For example, medical evacuation, head of state, and search and rescue.
inductive SpecialHandling
| altrv
| atfmx
| ffr
| fltck
| hazmat
| head
| hosp
| hum
| marsa
| medevac
| nonrvsm
| sar
| state
deriving DecidableEqDefinitions that relate to the aircraft used to conduct a flight. Note the distinction between flight and aircraft: flight is the operation between departure and destination that transports passengers and/or freight, aircraft is the physical airframe that carries the passengers and/or freight.
The registration identifies the physical aircraft as allocated by the authorising body. It appears as the tail markings on an aircraft. For GA flights, the aircraft identification is often the registration mark.
def Registration := Str 2 7
deriving DecidableEqThe number of aircraft that participate if the flight is a formation.
def NumberOfAircraft := NatMN 2 99
deriving DecidableEqAn aircraft type identifies the type of aircraft. For example, A388 is the type designator for an Airbus A380-800. Such designators are documented in ICAO Doc 8643.
def Doc8643.Designator := Str 2 4
deriving DecidableEqNot all aircraft types are listed in Doc 8643. In such cases they are presented as a free text name.
inductive AircraftType
| desig (_ : Doc8643.Designator)
| name (_ : FreeText)
deriving DecidableEqThe aircraft address is six hexadecimal characters, and uniquely identifies the airframe.
def AircraftAddress := Str 6 6
deriving DecidableEqPerformance data relating to the aircraft.
inductive AircraftPerformance
| a
| b
| c
| d
| e
| h
deriving DecidableEqThe wake turbulence category indicates the disturbance of the air caused by the aircraft, which affects other air traffic.
inductive WakeTurbulenceCategory
| h -- high
| m -- medium
| l -- low
deriving DecidableEqVertical distance may be expressed in metric or imperial measures.
inductive UnitOfVerticalDistance
| feet
| metres
deriving DecidableEqVertical distance may be expressed as a flight level (above the transition level) or an altitude (below the transition level).
inductive FlightLevelOrAltitude
| flightLevel
| altitude
deriving DecidableEqExpression of the vertical position of an aircraft.
structure VerticalPositionOfAircraft where
value : Int
uom : UnitOfVerticalDistance
type : FlightLevelOrAltitude
deriving DecidableEqUnit of horizontal distance. For this specification only nautical miles is required.
inductive UnitOfHorizontalDistance
| nm
deriving DecidableEqExpression of horizontal distance.
structure HorizontalDistance where
value : Nat
uom : UnitOfHorizontalDistance
deriving DecidableEqSpeed can be expressed in knots, kilometres per hour, or mach (fraction of the speed of sound).
inductive UnitOfSpeed
| kt
| kph
| mach
deriving DecidableEqSpeed can be:
- true airspeed - how fast the aircraft is moving through the body of air;
- indicated airspeed - the speed as indicated by the aircraft instruments;
- groundspeed - the speed of the aircraft with respect to the ground.
inductive SpeedDatum
| tas
| ias
| gspd
deriving DecidableEqAircraft speed is a value with respect to a unit of measurement and a datum.
structure AircraftSpeed where
value : Nat
uom : UnitOfSpeed
datum : SpeedDatum
inv : -- Ground speed cannot be expressed as a mach number
datum = .gspd → uom ≠ .mach
deriving DecidableEqTrue airspeed (TAS) is how fast the aircraft is moving through the body of air.
def TrueAirspeed := { spd : AircraftSpeed // spd.datum = .tas }
deriving DecidableEqLanding sites are recorded and assigned a unique identifier in ICAO Doc 7910.
def Doc7910.Designator := Str 4 4
deriving DecidableEqA waypoint is a named point used for identifying the path an aircraft follows.
def Waypoint := Str 2 5
deriving DecidableEqA relative point is a point indicated by its bearing and distance from a known point.
structure RelativePoint where
point : Waypoint
bearing : Geo.Direction
distance : HorizontalDistance
deriving DecidableEqPosition can be expressed by:
- the geographic position (latitude/longitude);
- a named (and documented) waypoint;
- a relative point.
inductive Position
| geo (_ : Geo.Point)
| wpt (_ : Waypoint)
| rel (_ : RelativePoint)
deriving DecidableEqThe named waypoint in a position (if there is one).
def Position.waypointOf : Position → Option Waypoint
| .wpt pt => pt
| _ => noneAn aircraft needn't always take off or land at a documented point. Sometimes a descriptive name and lat/long are given.
structure NameAndPosition where
name : FreeText
position : Position
deriving DecidableEqA landing site is identified by its ICAO designator or name and position.
inductive LandingSite
| desig (_ : Doc7910.Designator)
| namePos (_ : NameAndPosition)
deriving DecidableEqThe air space through which aircraft transit is divided into areas called Flight Information Regions (FIR). They are documented in ICAO Doc 7910.
def Doc7910.FIRDesignator := Str 4 4
deriving DecidableEqThe communication, navigation and surveillance equipment held by aircraft and the capabilities of the equipment are identified by codes documented in PANS-ATM.
Communication, navigation and approach aid equipment and capabilities.
inductive CommNavAppCode
| s
| a
| b
| c
| d
| e1
| e2
| e3
| f
| g
| h
| i
| j1
| j2
| j3
| j4
| j5
| j6
| j7
| k
| l
| m1
| m2
| m3
| o
| p1
| p2
| p3
| p4
| p5
| p6
| p7
| p8
| p9
| r
| t
| u
| v
| w
| x
| y
| z
deriving DecidableEqSurveillance equipment and capabilities.
inductive SurveillanceCode
| a
| c
| e
| h
| i
| l
| p
| s
| x
| b1
| b2
| u1
| u2
| v1
| v2
| d1
| g1
deriving DecidableEqPerformance Based Navigation (PBN) codes.
inductive PBNCode
| a1
| b1
| b2
| b3
| b4
| b5
| b6
| c1
| c2
| c3
| c4
| d1
| d2
| d3
| d4
| l1
| o1
| o2
| o3
| o4
| s1
| s2
| t1
| t2
deriving DecidableEqSelective Calling (SELCAL) code.
def SelcalCode := Str 4 4
deriving DecidableEqA designator for an air route (a fixed route in 3D space that an aircraft can follow).
def RouteDesignator := Str 2 7
deriving DecidableEqDesignator for an Air Traffic Services authority.
def ATSUnit := Str 4 4
deriving DecidableEqAddress on the global Aeronautical Fixed Telecommunications Network (AFTN).
def AFTNAddress := Str 8 8
deriving DecidableEq
end Core