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

SB_UAS_9

Specification Description

The UAS's position will exist on Earth GPS coordinates. Lat will be bounded in (-90, 90) deg and Long will be bounded in (-180, 180) deg at all instances

Signals Required

Lat, Long

Boolean Conversion of Signals to Atomic Inputs 

Lat_gt_90: Lat > -90
Lat_lt_90: Lat < 90
Long_gt_180: Long > -180
Long_lt_180: Long < 180

MLTL Specification

☐[0,M] (Lat_gt_90 ∧ Lat_lt_90 ∧ Long_gt_180 ∧ Long_lt_180)

Fault Explanation

UAS is outside of latitude and/or longitude earth bounds.

Additional Notes

Figures

Figure 1: Latitude and Longitude with physically possible bounds.
Figure 2: R2U2's output of SB_UAS_9, showing that the latitude and longitude never exceed the bounds.
Figure 3: A fault injected into the latitude and longitude to exceed the upper bounds.
Figure 4: R2U2's output of Fig. 3, showing it was able to detect the injected fault.