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_19

Specification Description

Conflicting flight plan IDs (conUAS_A and conUAS_B) must be different IDs

Signals Required

conUAS_A, conUAS_B

Boolean Conversion of Signals to Atomic Inputs

conUASa_neq_conUASb: conUAS_A ≠ conUAS_B						

MLTL Specification

conUASa_neq_conUAS

Fault Explanation

You cannot have a conflict with yourself

Additional Notes

Figures