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_UTM_6
Specification Description
All altitude (fpAlt) waypoints of any UAS's telemetry data will be bounded between 0.0 and ALT_UB.
Signals Required
fpAlt
Boolean Conversion of Signals to Atomic Inputs
fpAlt_leq_AltUB = 1;
for(i = 0; i < NumUAS; i++)
{
// if UAS i's fpAlt is greater than the upper bounded
// and the value is not "nan"
for(j = 0; j < NumWps[i]; j++)
{
if((fpAlt[i,j] > AltUB) && (fpAlt[i,j] == fpAlt[i,j])
{
fpAlt_leq_AltUB = 0;
}
}
}
fpAlt_geq_AltLB = 1;
for(i = 0; i < NumUAS; i++)
{
// if UAS i's fpAlt is less than the lower bounded
// and the value is not "nan"
for(j = 0; j < NumWps[i]; j++)
{
if((fpAlt[i,j] < AltLB) && (fpAlt[i,j] == fpAlt[i,j])
{
fpAlt_geq_AltLB = 0;
}
}
}
MLTL Specification
Original: fpAlt_leq_AltLB ∧ fpAlt_geq_AltLB
Fault Explanation
Any waypoint from the flight plan should be within the UTM's airspace
Additional Notes