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_5

Specification Description

The flight time will be bounded by FT_OR_MAX at all instances.

Signals Required

Time

Boolean Conversion of Signals to Atomic Inputs 

FlightTime = Time - StartTime
FlightTime_leq_MAX: FlightTime ≤ FT_OR_MAX

MLTL Specification

☐[0,M] (FlightTime_leq_MAX)

Fault Explanation

FlightTime is exceeding maximum possible flighttime

Additional Notes

FT_OR_MAX based on maximum flight time while hovering in the air in ideal conditions (~2 hours)

Figures

Figure 1: Hours, Minutes, and Seconds of the Vapor 55 internal clock.
Figure 2: R2U2's output for OR_UAS_5, showing that the time never exceeded the maximum Flight Time.
Figure 3: Injected fault into hours, increasing it from 13 to 15.
Figure 4: R2U2's output, showing it detecte the jump in time and that it exceeded the maximum flight time.