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_2

Specification Description

A UAS reference waypoint (wpLat, wpLon) will eventually change to the next flight plan waypoint (fpLat, fpLon)

Signals Required

wpLat, wpLon,fpLat, fpLon

Boolean Conversion of Signals to Atomic Inputs

atomics_vector[38] = 1;
if((wpLat != prevWpLat) || (wpLon != prevWpLon)){
   i = 0; j = 0; k = 0;
   for(i = 0; i < NumWp; i++) {
        if(wpLat == fpLat[i]) {
            j = i;}
        if(prevWpLat == fpLat[i]){
            k = i; }}
    if((j < k) && (j != -1) && (k != -1)){
        atomics_vector[37] = 0;}
}						

MLTL Specification

♢[0,M] (wpLat_eq_fpLat ∧ wpLon_eq_fpLon)

Fault Explanation

The order the UAS progresses through waypoints should be upheld

Additional Notes

Figures