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_4

Specification Description

The Altitude (Alt in AGL) will be bounded by ALT_OR_MAX but if it exceeds, allow 3 timesteps to recover.

Signals Required

Alt

Boolean Conversion of Signals to Atomic Inputs 

Alt_leq_MAX: Alt ≤ ALT_OR_MAX

MLTL Specification

¬☐[0,3] ¬(Alt_leq_MAX)

Fault Explanation

Altitude is exceeding maximum altitude

Additional Notes

The altitude must be below a certain threshold and above ground.

Figures

Figure 1: Altitude of the Vapor 55 in meters.
Figure 2: R2U2's output of OR_UAS_4, showing the altitude remained inside bounds the entire time.
Figure 3: Injected fault into Altitude, exceeding the upper bound.
Figure 4: R2U2's output, showing it caught the fault.