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

IS_UAS_1

Specification Description

Since the altimeter and the barometer both can derive the air pressure, the error between these two measurements of pressure will be less than ERROR_PRES. If it is not, allow 3 time steps to recover

Signals Required

Pres (Barometer), Alt (GPS)

Boolean Conversion of Signals to Atomic Inputs 

Pres_lt_MaxPresErr: PRES_baro < PRES_GPSder + ERROR_PRES
Pres_gt_MinPresErr: PRES_baro > PRES_GPSder - ERROR_PRES

MLTL Specification

¬☐[0,3] ¬(Pres_lt_MaxPresErr ∧ Pres_gt_MinPresErr)

Fault Explanation

The Pressure measured from the barometer doesn't match up with the pressure calculated from the GPS.

Additional Notes

Relationship derived from hydrostatic equation and equation of state.

Figures

Figure 1: Pressure readings returned from the Barometer to the UAS
Figure 2: R2U2 Output for specification IS_UAS_1, confirming the pressure from the Barometer and and pressure derived from the GPS never differ by more than than ERROR_PRES.
Figure 3: Since Fig. 1 had no pressure differences that exceeded ERROR_PRES, we manually injected a fault into a the barometer output (~1500-1750 sec).
Figure 4: R2U2's output of specification IS_UAS_1 with the injected fault, showing that R2U2 catches the injected fault when the difference between the barometer's pressure and the pressure derived from the GPS jumps out of bounds.