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_UTM_17

Specification Description

If there is an en route conflict detected between two UAS (conUAS_A and conUAS_B), then the estimated Start time and the estimated End time of a flight plan must overlap for the two UAS

Signals Required

conUAS_A, conUAS_B, Start, End

Boolean Conversion of Signals to Atomic Inputs

StartA_leq_StartB: Start(conUAS_A) ≤ Start(conUAS_B)
StartA_leq_EndB: Start(conUAS_A) ≤ End(conUAS_B)
StartB_leq_EndA: Start(conUAS_B) ≤ End(conUAS_A)

MLTL Specification

(StartA_leq_StartB ∧ StartB_leq_EndA) ∨ (¬StartA_leq_StartB ∧ StartA_leq_EndB)

Fault Explanation

You should not have a conflict with anyone who is not in the air

Additional Notes

Figures

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