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_1

Specification Description

All wpLat will be bounded between -90 and 90 degrees

Signals Required

wpLat

Boolean Conversion of Signals to Atomic Inputs

wpLat_leq_MaxLatUB: wpLat ≤ MaxLatUB
wpLat_geq_MinLatLB: wpLat ≥ MinLatLB

MLTL Specification

¬☐[0,M] ¬(wpLat_leq_MaxLatUB ∧ wpLat_geq_MinLatLB)

Fault Explanation

Latitude is outside of path between way points

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