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_1

Specification Description

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

Signals Required

Ang, Vel, Lat, Lon

Boolean Conversion of Signals to Atomic Inputs 

Ang_leq_90: Ang ≤ 90.0
Ang_geq_0: Ang ≥ 0.0
Vel_gt_0: Vel > 0.0
Lat_minus_Prev_gt_0: Lat - PrevLat > 0
Lon_minus_Prev_lt_0: Lon - PrevLon < 0

MLTL Specification

(Ang_leq_90 ∧ Ang_geq_0 ∧ Vel_gt_0) → (Lat_minus_Prev_gt_0 ∧ Lon_minus_Prev_lt_0)

Fault Explanation

The UAS's bearing is between 0 and 90 degrees, but the Latitude is decreasing and/or the Longitude is increasing whearas they should be increasing and decreasing 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