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

IS_UTM_1

Specification Description

The Time of any given telemetry stream should be bounded within the flight plan's estimated Start and End times

Signals Required

Time,Start, End

Boolean Conversion of Signals to Atomic Inputs 

Time_geq_Start: Time ≥ Start
Time_leq_End: Time ≤ End

MLTL Specification

☐ (Time_geq_Start ∧ Time_leq_End)

Fault Explanation

FlightTime has exceeded the start or end time

Additional Notes

Figures

Figure 1: Caption
Figure 2: Caption
Figure 3: Caption
Figure 4: Caption
Figure 5: Caption