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_2

Specification Description

If a UAS takes off, eventually it will land in all cases.

Signals Required

Phase, Subphase

Boolean Conversion of Signals to Atomic Inputs

Phase_eq_Takeoff: Phase == "Takeoff"
Phase_eq_Landing: Phase == "Landing"

MLTL Specification

Phase_eq_Takeoff → ♢[0,M] (Phase_eq_Landing)

Fault Explanation

Landing did not occur after takeoff.

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