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

SB_UAS_7

Specification Description

The Time will be bounded between 0 and 23:59:59 at all instances

Signals Required

Time

Boolean Conversion of Signals to Atomic Inputs 

Time_lt_24: Time ≤ 23:59:59
Time_geq_0: Time ≥ 0:00:00

MLTL Specification

☐[0,M] (Time_lt_24 ∧ Time_geq_0)

Fault Explanation

Clock is outside of physical possibility

Additional Notes

Time from 24 hour clock onboard UAS

Figures

Figure 1: Graph of the Hours, Minutes, and Seconds of the Vapor 55's internal clock.
Figure 2: R2U2's output showing that the time is always a realistic number.
Figure 3: An injected fault where the seconds are negative.
Figure 4: R2U2's output of Fig. 3, showing that R2U2 was able to detect the injected fault.