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_4
Specification Description
Flight_Plan_IDs, issued from the UTM server, may only ever increment (to make sure no two UAS have the same Flight_Plan_ID)
Signals Required
Flight_Plan_ID
Boolean Conversion of Signals to Atomic Inputs
fpID_leq_PrevfpID: Flight_Plan_ID ≤ PrevFlight_Plan_ID
MLTL Specification
☐ (fpID_leq_PrevfpID)
Fault Explanation
Overflow of Flight_Plan_ID counter
Additional Notes
Figures




