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_5

Specification Description

If a UAS is flying toward a CRUISE waypoint, it will maintain its speed.

Signals Required

Subphase, AccD, AccE, AccN

Boolean Conversion of Signals to Atomic Inputs

Subphase_eq_Cruise: Subphase == "Cruise"
AccD_eq_0: AccD == 0
AccN_eq_0: AccN == 0
AccE_eq_0: AccE == 0

MLTL Specification

Subphase_eq_Cruise → ♢[0,M] (AccD_eq_0 ∧ AccN_eq_0 ∧ AccE_eq_0)

Fault Explanation

UAS is either accelerating or decelerating towards a Cruise Waypoint.

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