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_2

Specification Description

The Roll measurement will be bounded between -45 and 45 degrees, but if it exceeds it, allow 3 timesteps to recover.

Signals Required

Roll

Boolean Conversion of Signals to Atomic Inputs 

Roll_geq_45: Roll ≥ -45
Roll_leq_45: Roll ≤ 45

MLTL Specification

¬☐[0,3] ¬(Roll_geq_45 ∧ Roll_leq_45)

Fault Explanation

Roll is exceeding flight bounds

Additional Notes

45 degrees is highly conservative

Figures

Figure 1: Roll in degrees the Vapor 55 experiences.
Figure 2: R2U2's output of OR_UAS_2, confirming the roll stayed within bounds the entire time.
Figure 3: Graph showing an injected fault into Roll, pushing it above the upper bound.
Figure 4: R2U2's output with the fault, showing that it catches the injected fault.