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_GCS_5

Specification Description

All fpLat will be bounded between -90 and 90 degrees

Signals Required

fpLat

Boolean Conversion of Signals to Atomic Inputs

fpLat_leq_MaxLatUB: fpLat ≤ MaxLatUB
fpLat_geq_MinLatLB: fpLat ≥ MinLatLB

MLTL Specification

¬☐[0,M] ¬(fpLat_leq_MaxLatUB ∧ fpLat_geq_MinLatLB)

Fault Explanation

Latitude is outside of predefined flightpath

Additional Notes

All Latitude and Longitude values should be actual Earth locations

Figures

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