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

SB_UAS_2

Specification Description

The Roll measurement will be bounded in (-180,180] degrees at all instances

Signals Required

Roll

Boolean Conversion of Signals to Atomic Inputs 

Roll_gt_180: Roll > -180
Roll_leq_180: Roll ≤ 180

MLTL Specification

☐[0,M] (Roll_gt_180 ∧ Roll_leq_180)

Fault Explanation

Measured roll is outside of physical possibility

Additional Notes

Based on UAS onboard telemetry definition for roll

Figures

Figure 1: Roll of the Vapor 55.
Figure 2: R2U2's output of SB_UAS_2, showing that the roll never exceeded the sensor's bounds.
Figure 3: A fault injected into the roll of the Vapor.
Figure 4: R2U2's output of Fig. 3, showing that it was able to detect the injected fault.