Integrating Runtime Verification into an
Automated UAS Traffic Management System

Matthew Cauwels, Abigail Hammer, Benjamin Hertz, Phillip H. Jones, Kristin Y. Rozier

This webpage contains supplementary specifications for "Integrating Runtime Verification into an
Automated UAS Traffic Management System" by M. Cauwels, A. Hammer, B. Hertz, P. H. Jones, and K. Y. Rozier

PM_UTM_4

Specification Description

If the Ang from a UAS's telemetry is between 270 and 360 degrees, then, if the UAS's Vel is greater than zero, the UAS's Lat and Lon should be decreasing each telemetry stream

Signals Required

Ang, Vel, Lat, Lon

Boolean Conversion of Signals to Atomic Inputs 

Ang_geq_270: Ang ≥ 270.0
Ang_leq_360: Ang ≤ 360.0
Vel_gt_0: Vel > 0.0
Lat_minus_Prev_lt_0: Lat - PrevLat < 0
Lon_minus_Prev_lt_0: Lon - PrevLon < 0

MLTL Specification

(Ang_geq_270 ∧ Ang_leq_360 ∧ Vel_gt_0) → (Lat_minus_Prev_lt_0 ∧ Lon_minus_Prev_lt_0)

Fault Explanation

The UAS's bearing is between 270 and 360 degrees, but the Latitude and/or Longitude is increasing whearas they should be decreasing

Additional Notes

Assuming the UTM is operating in North America, there should be a correlation between heading and Lat/Lon, if the UAS's velocity is nonzero

Figures

Figure 1: Caption
Figure 2: Caption
Figure 3: Caption
Figure 4: Caption
Figure 5: Caption