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_16

Specification Description

A conflicting flight plan ID (conUAS_A or conUAS_B) must always greater than 0 and less than the maximum number of assigned flight plan IDs

Signals Required

conUAS_A, conUAS_B, Flight_Plan_ID

Boolean Conversion of Signals to Atomic Inputs

conUASa_geq_MaxFP: conUAS_A ≥ max(Flight_Plan_ID)
conUASb_geq_MaxFP: conUAS_B ≥ max(Flight_Plan_ID)

MLTL Specification

conUASa_geq_MaxFP ∧ conUASb_geq_MaxFP

Fault Explanation

You cannot have a conflict with an unassigned flight plan

Additional Notes

Figures