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_GCS_4

Specification Description

The incoming telemetry data's Time field should be within MAX_RATE seconds of the previous telemetry data's Time field

Signals Required

Time, PrevTime

Boolean Conversion of Signals to Atomic Inputs

TimeDif_leq_MaxTime: (Time - PrevTime) ≤ MAX_RATE

MLTL Specification

¬☐[0,3] (¬TimeDif_leq_MaxTime)

Fault Explanation

There have been many dropped packages in a row

Additional Notes

Make sure we have timely updates from the UAS

Figures