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_8

Specification Description

The flight time will be bounded between 0 and FT_SENS_MAX at all instances

Signals Required

Time

Boolean Conversion of Signals to Atomic Inputs 

FlightTime = Time - StartTime
FlightTime_lt_MAX: FlightTime < FT_SENS_MAX
FlightTime_geq_MAX: FlightTime ≥ 0

MLTL Specification

☐[0,M] (FlightTime_lt_MAX ∧ FlightTime_geq_MAX)

Fault Explanation

Flight time has exceeded the possibly flight time the UAS can fly

Additional Notes

FT_SENS_MAX based on longest possible operating time of battery (most likely while aircraft is in standby on ground)

Figures

Figure 1: Graph of the Hours, Minutes, and Seconds recorded at each time step.

Additional Figures for SB_UAS_8 are currently being generated.