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_12

Specification Description

The FlightMode of the UAS will be limited to the following strings at all instances: Automatic, Home

Signals Required

FlightMode

Boolean Conversion of Signals to Atomic Inputs 

FlightMode_eq_Automatic: FlightMode == Automatic
FlightMode_eq_Home: FlightMode == Home

MLTL Specification

☐[0,M] (FlightMode_eq_Automatic ∨ FlightMode_eq_Home)

Fault Explanation

Flightmode is not one of predefined strings. Can only be Home or Automatic

Additional Notes

Based on all possible states the UAS FlightMode can enter

Figures

Figure 1: Graph of FlightMode strings.
Figure 2: R2U2's output showing that FlightMode never deviated from predefined strings.
Figure 3: Fault injected where FlightMode is set to "Nonexistant_String".
Figure 4: R2U2's output of Fig. 3, showing that R2U2 is able to detect the injected fault.