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

RC_UTM_2

Specification Description

Once the Status of a flight plan is APPROVED, it can only transition from APPROVED to REPLACED; never APPROVED to REJECTED

Signals Required

Status

Boolean Conversion of Signals to Atomic Inputs

Status_eq_Rejected: Status == REJECTED
Status_eq_Approved: Status == APPROVED

MLTL Specification

Status_eq_Rejected → ☐ (¬Status_eq_Approved)

Fault Explanation

REJECTED flightplan has moved to APPROVED

Additional Notes

Figures