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

CS_GCS_1

Specification Description

The reference waypoint (wpLat, wpLon) will eventually change to a new reference waypoint

Signals Required

wpLat, wpLon

Boolean Conversion of Signals to Atomic Inputs

wpLat_neq_prevWpLat: wpLat ≠ prevWpLat
wpLon_new_prevWpLon: wpLon ≠ prevWpLon						

MLTL Specification

♢[0,M](wpLat_neq_preWpLat ∧ wpLon_neq_prevWpLon)

Fault Explanation

The UAS should progress through waypoints (not be stuck at one waypoint)

Additional Notes

Figures