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_4

Specification Description

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

Signals Required

Yaw

Boolean Conversion of Signals to Atomic Inputs 

Yaw_gr_180: Yaw > -180
Yaw_leq_180: Yaw ≤ 180

MLTL Specification

☐[0,M] (Yaw_gr_180 ∧ Yaw_leq_180)

Fault Explanation

Measured yaw is outside of physical possibility

Additional Notes

Based on UAS onboard telemetry definition for yaw

Figures

Figure 1: Yaw angle of Vapor 55.
Figure 2: R2U2's output of SB_UAS_4, showing that the Yaw angle never exceeded the sensor's bounds.
Figure 3: Fault injected into Yaw, exceeding the upper bounds.
Figure 4: R2U2's output, showing it detected the injected fault.