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_1

Specification Description

The motor RPM will be bounded between 0 and RPM_SENS_MAX at all instances

Signals Required

RPM

Boolean Conversion of Signals to Atomic Inputs 

RPM_geq_0: RPM ≥ 0.0
RPM_leq_MAX: RPM ≤ RPM_SENS_MAX

MLTL Specification

☐[0,M] (RPM_geq_0 ∧ RPM_leq_MAX)

Fault Explanation

Motor RPM is not within bounds

Additional Notes

RPM_SENS_MAX would be obtained from physical max RPM rotor can produce

Figures

Figure 1: RPM of the Vapor 55's motor.
Figure 2: R2U2's output of SB_UAS_1, showing that the RPM never exceeded physical bounds.
Figure 3: An injected fault into the RPM.
Figure 4: R2U2's output, showing it was able to detect the injected fault.