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_2

Specification Description

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

Signals Required

Ang, Vel, Lat, Long

Boolean Conversion of Signals to Atomic Inputs 

Ang_geq_180: Ang ≥ 180.0
Ang_leq_90: Ang ≤ 90.0
Vel_gt_0: Vel > 0.0
Lat_minus_Prev_gt_0: Lat - PrevLat > 0
Lon_minus_Prev_gt_0: Lon - PrevLon > 0

MLTL Specification

(Ang_geq_180 ∧ Ang_leq_90 ∧ Vel_gt_0) → (Lat_minus_Prev_gt_0 ∧ Lon_minus_Prev_gt_0)

Fault Explanation

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

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