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_3

Specification Description

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

Signals Required

Ang, Vel, Lat, Lon

Boolean Conversion of Signals to Atomic Inputs 

Ang_geq_180: Ang ≥ 180.0
Ang_leq_270: Ang ≤ 270.0
Vel_gt_0: Vel > 0.0
Lat_minus_Prev_lt_0: Lat - PrevLat < 0
Lon_minus_Prev_gt_0: Lon - PrevLon > 0

MLTL Specification

(Ang_geq_180 ∧ Ang_leq_270 ∧ Vel_gt_0) → (Lat_minus_Prev_lt_0 ∧ Lon_minus_Prev_gt_0)

Fault Explanation

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

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