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

Figure 1: Caption
Figure 2: Caption
Figure 3: Caption
Figure 4: Caption
Figure 5: Caption