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_GCS_3

Specification Description

Once the Status of a flight plan is REPLACED, it can never become APPROVED

Signals Required

Status

Boolean Conversion of Signals to Atomic Inputs

Status_eq_Approved: Status == APPROVED
Status_eq_Replaced: Status == REPLACED

MLTL Specification

Status_eq_Replaced → ☐ (¬Status_eq_Approved)

Fault Explanation

REPLACED flightplan has moved to APPROVED

Additional Notes

Defines the valid transitions for the Status variable

Figures