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_GCS_1
Specification Description
The Status of a flight plan will always be either: ACCEPTED, REJECTED, or REPLACED
Signals Required
Status
Boolean Conversion of Signals to Atomic Inputs
Status_eq_Accepted: Status == ACCEPTED
Status_eq_Rejected: Status == REJECTED
Status_eq_Replaced: Status == REPLACED
MLTL Specification
Status_eq_Accepted ∨ Status_eq_Rejected ∨ Status_eq_Replaced
Fault Explanation
Flightplan status is not a predefined string
Additional Notes
Limiting the type of response the UTM can send for a flight plan
Figures




