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_UAS_6

Specification Description

The Temp of the UAS will be bounded between TEMP_OR_MIN and TEMP_OR_MAX, but if it is not, allow 3 timesteps to recover.

Signals Required

Temp

Boolean Conversion of Signals to Atomic Inputs 

Temp_leq_MAX: Temp ≤ TEMP_OR_MAX
Temp_geq_MIN: Temp ≥ TEMP_OR_MIN

MLTL Specificaiton

¬☐[0,3] ¬(Temp_leq_MIN ∧ Temp_geq_MIN)

Fault Explanation

Ambient temperature is exceeding flight bounds

Additional Notes

TEMP_OR_MIN and TEMP_OR_MAX based on acceptable flight conditions (primarily dependent on battery operating conditions)

Figures

Figure 1: Graph of the Ambient Temperature onboard the Vapor 55.

Figures are currently being generated for OR_UAS_6 data