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_1

Specification Description

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

Signals Required

Status

Boolean Conversion of Signals to Atomic Inputs

Status_eq_Rejected: Status == REJECTED

MLTL Specification

Status_eq_Rejected → ☐ (Status_eq_Rejected)

Fault Explanation

REJECTED flightplan has moved to either APPROVED or REPLACED

Additional Notes

Defines the valid transitions for the Status variable

Figures