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

OR_GCS_12

Specification Description

The latitude (Lat) of any UAS's telemetry data will be bounded between LAT_LB and LAT_UB

Signals Required

Lat

Boolean Conversion of Signals to Atomic Inputs 

Lat_leq_LatUB: Lat ≤ LatUB
Lat_geq_LatLB: Lat ≥ LatLB

MLTL Specification

Lat_leq_LatLB ∧ Lat_geq_LatLB

Fault Explanation

Any telemetry point should be within the UTM's airspace

Additional Notes

Figures

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

Integrating Runtime Verification into an Automated UAS Traffic Management System

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

OR_GCS_12

Specification Description

The latitude (Lat) of any UAS's telemetry data will be bounded between LAT_LB and LAT_UB.

Signals Required

Lat

Boolean Conversion of Signals to Atomic Inputs

Lat_leq_LatUB: Lat <= LatUB

Lat_geq_LatLB: Lat >= LatLB

MLTL Specification

Original: Lat_leq_LatLB & Lat_geq_LatLB

Updated: G[0,3] (Lat_leq_LatLB & Lat_geq_LatLB)

Fault Explanation

Any telemetry point should be within the UTM's airspace

Additional Notes