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_3

Specification Description

All Lat will be bounded between -90 and 90 degrees

Signals Required

Lat

Boolean Conversion of Signals to Atomic Inputs

Lat_leq_MaxLatUB: Lat ≤ MaxLatUB
Lat_geq_MinLatLB: Lat ≥ MinLatLB

MLTL Specification

¬☐[0,M] ¬(Lat_leq_MaxLatUB ∧ Lat_geq_MinLatLB)

Fault Explanation

Latitude is outside of physical possiblity

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