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

CS_UAS_3

Specification Description

The UAS will always take-off before it lands in all cases

Signals Required

Phase, Subphase

Boolean Conversion of Signals to Atomic Inputs

Takeoff_Time_lt_Landing_Time: Takeoff_Time < Landing_Time

MLTL Specification

☐[0,M] (Takeoff_Time_lt_Landing_Time)

Fault Explanation

The UAS has landed before taking off.

Additional Notes

Until such a time that a test flight with the Vapor 55 can be completed, this specification is unable to be fully tested.

Figures