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

OR_GCS_1

Specification Description

The Status of a flight plan will always be either: ACCEPTED, REJECTED, or REPLACED

Signals Required

Status

Boolean Conversion of Signals to Atomic Inputs

Status_eq_Accepted: Status == ACCEPTED
Status_eq_Rejected: Status == REJECTED
Status_eq_Replaced: Status == REPLACED

MLTL Specification

Status_eq_Accepted ∨ Status_eq_Rejected ∨ Status_eq_Replaced

Fault Explanation

Flightplan status is not a predefined string

Additional Notes

Limiting the type of response the UTM can send for a flight plan

Figures

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