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_UTM_5

Specification Description

The rate at which an individual UAS's telemetry data is received by the UAS will be once per second while the UAS is in flight

Signals Required

ID, Time

Boolean Conversion of Signals to Atomic Inputs

Time_geq_PrevTime: Time(ID) ≥ PrevTime(ID) + 3

MLTL Specification

☐[0,3] Time_geq_PrevTimeMargin

Fault Explanation

Loss of telemetry transmission for UAS ID

Additional Notes

Telemetry is used to check for loss of communications

Figures

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