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_2

Specification Description

The Start time of any flight plan must be less than the flight plan's End time

Signals Required

Start, End

Boolean Conversion of Signals to Atomic Inputs 

Start_leq_End: Start ≤ End

MLTL Specification

Start_leq_End

Fault Explanation

The user should not be able to say they landed before they took off

Additional Notes

Figures

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