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_6

Specification Description

The UTM will return a Status response to a flight plan request within UTM_MAX_FP_RESPONSE_TIME

Signals Required

Status, Time_Filed

Boolean Conversion of Signals to Atomic Inputs

Status_eq_Rejected: Status == REJECTED
Status_eq_Approved: Status == APPROVED
Status_eq_Replaced: Status == REPLACED
TimeFiledDiff_geq_Margin: Time - TimeFiled ≥ Margin

MLTL Specification

☐[0,3] [ (¬Status_eq_Rejected ∧ ¬ Status_eq_Approved ∧ ¬Status_eq_Replaced) ∧ TimeFiledDiff_geq_Margin]

Fault Explanation

Failure of UTM to return UAS ID's flight plan Status

Additional Notes

The UTM should have timely responses to flight plans

Figures