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_3

Specification Description

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

Signals Required

Pitch

Boolean Conversion of Signals to Atomic Inputs 

Pitch_gr_180: Pitch > -180
Pitch_leq_180: Pitch ≤ 180

MLTL Specification

☐[0,M] (Pitch_gr_180 ∧ Pitch_leq_180)

Fault Explanation

Measured pitch is outside of physical possibility

Additional Notes

Based on UAS onboard telemetry definition for pitch

Figures

Figure 1: Pitch of the Vapor 55.
Figure 2: R2U2's output, showing that the Pitch stayed within the sensor's bounds.
Figure 3: An injected fault into the pitch of the Vapor.
Figure 4: R2U2's output, showing that it was able to detect the injected fault.