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_5

Specification Description

All longitude (fpLon) waypoints of any UAS's telemetry data will be bounded between LON_LB and LON_UB

Signals Required

fpLon

Boolean Conversion of Signals to Atomic Inputs 

fpLon_leq_LonUB: fpLon ≤ Lon_UB
fpLon_geq_LonLB: fpLon ≥ Lon_UB

MLTL Specification

fpLat_leq_LatUB ∧ pfLat_geq_LatLB

Fault Explanation

Any waypoint from the flight plan 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_5

Specification Description

All longitude (fpLon) waypoints of any UAS's telemetry data will be bounded between LON_LB and LON_UB

Signals Required

fpLon 

fpLon_leq_LonUB: fpLon ≤ Lon_UB
fpLon_geq_LonLB: fpLon ≥ Lon_UB

MLTL Specification

fpLon_leq_LonUB ∧ fpLon_geq_LongLB

Fault Explanation

Any waypoint from the flight plan should be within the UTM's airspace

Additional Notes

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