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_2

Specification Description

The conStart and conEnd times of a conflict should be bounded within the flight plan's estimated Start and End times

Signals Required

conStart, conEnd, Start, End

Boolean Conversion of Signals to Atomic Inputs 

conStart_geq_Start: conStart ≥ Start
conEnd_leq_End: conEnd ≤ End

MLTL Specification

☐ (conStart_geq_Start ∧ conEnd_leq_End)

Fault Explanation

Conflict Times exceed the planned flight time

Additional Notes

Figures

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