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_21
Specification Description
The longitude (conLon) of any conflict will be bounded between LonLB and LonUB
Signals Required
conLon
Boolean Conversion of Signals to Atomic Inputs
conLon_leq_LonUB = 1;
for(i = 0; i < NumUAS; i++)
{
// if UAS i's conLon is greater than the upper bounded
// and the value is not "nan"
if((conLon[i] > LonUB) && (conLon[i] == conLon[i])
{
conLon_leq_LonUB = 0;
}
}
conLon_geq_LonLB = 1;
for(i = 0; i < NumUAS; i++)
{
// if UAS i's conLon is less than the lower bounded
// and the value is not "nan"
if((conLon[i] < LonLB) && (conLon[i] == conLon[i])
{
conLon_geq_LonLB = 0;
}
}
MLTL Specification
Original: conLon_leq_LonUB ∧ conLon_geq_LonLB
Updated: ☐[0,3] (conLon_leq_LonUB ∧ conLon_geq_LonLB)
Fault Explanation
Any conflict should be within the UTM's airspace
Additional Notes
Figures




