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
Complete Specification List
This webpage presents the complete list of specifications developed for the UTM system, whereas only a few specifications were listed within Table III.
To view more information about any given specification, click on the name of the specification.
| UAS Operating Range Specifications | Name | Description | Specification |
|---|---|---|
| UAS_OR_1 | The motor RPM will be bound by RPM_OR_MIN and RPM_OR_MAX while Subphase is not equal to Landed, Test Actuators, or <undefined> | (Subphase_neq_Undefined ∧ Subphase_neq_TestActuators ∧ Subphase_neq_Landed) → ¬☐[0,3] ¬(RPM_leq_MAX ∧ RPM_geq_MIN) |
| UAS_OR_2 | The Roll measurement will be bounded between -45 to 45 degrees, but if it exceeds it, allow 3 timesteps to recover | ¬☐[0,3] ¬(Roll_geq_45 ∧ Roll_leq_45) |
| UAS_OR_3 | The Pitch measurement will be bounded between -45 to 45 degrees, but if it exceeds it, allow 3 timesteps to recover | ¬☐[0,3] ¬(Pitch_geq_45 ∧ Pitch_leq_45) |
| UAS_OR_4 | The Altitude (Alt in AGL) will be bounded by ALT_OR_MAX, but if it exceeds it, allow 3 timesteps to recover | ¬☐[0,3] ¬(Alt_leq_MAX) |
| UAS_OR_5 | The flight time will be bounded by FT_OR_MAX at all instances | ☐[0,M] (FlightTime_leq_MAX) |
| UAS_OR_6 | The Temp of the UAS will be bounded between TEMP_OR_MIN and TEMP_OR_MAX, but if it is not, allow 3 timesteps to recover | ¬☐[0,3] ¬(Temp_leq_MIN ∧ Temp_geq_MIN) |
| UAS_OR_7 | The TempE1 of the UAS will be bounded between TEMPE1_OR_MIN and TEMPE1_OR_MAX, but if it is not, allow 3 timesteps to recover | ¬☐[0,3] ¬(TempE2_leq_MIN ∧ TempE1_geq_MIN) |
| UAS_OR_8 | The TempE2 of the UAS will be bounded between TEMPE2_OR_MIN and TEMPE2_OR_MAX, but if it is not, allow 3 timesteps to recover | ¬☐[0,3] ¬(TempE2_leq_MIN ∧ TempE1_geq_MIN) |
| UAS_OR_9 | The Pres of the UAS will be bounded between PRES_OR_MIN and PRES_OR_MAX, but if it is not, allow 3 timesteps to recover | ¬☐[0,3] ¬(Pres_leq_MAX ∧ Pres_geq_MIN) |
| UAS_OR_10 | The magnitude of the horizontal velocity components (VelN, VelE) will be bounded between 0 and VELH_OR_MAX at all instances | ¬☐[0,3] ¬(VelH_Mag_leq_MAX ∧ VelH_Mag_geq_0) |
| UAS_OR_11 | The magnitude of the individual velocity components VelD will be bounded between 0 and VELD_OR_MAX at all instances | ☐[0,3] ¬(VelD_Mag_leq_MAX ∧ VelD_Mag_geq_0) |
| UAS_OR_12 | The magnitude of the individual position components (PosN, PosE, PosD) will be bounded between 0 and DIST_OR_MAX, but if it is not, allow 3 timesteps to recover | ¬☐[0,3] ¬(PosMag_lt_MAX) |
| UAS_OR_13 | The UAS's position will be bounded within a circle of radius MAX_RECEIVER_DIST | ☐[0,M] (PosMag_leq_MAX) |
| GCS Operating Range Specifications | Name | Description | Specification |
|---|---|---|
| GCS_OR_1 | The Status of a flight plan will always be either: ACCEPTED, REJECTED, or REPLACED | Status_eq_Accepted ∨ Status_eq_Rejected ∨ Status_eq_Replaced |
| GCS_OR_2 | The Start time of any flight plan must be less than the flight plan's End time | Start_leq_End |
| GCS_OR_3 | The Start time of any flight plan should be greater than the Time_Filed of the flight plan | Start_geq_TimeFiled |
| GCS_OR_4 | All latitude (fpLat) waypoints of any UAS's flight plan will be bounded between LAT_LB and LAT_UB | fpLat_leq_LatUB ∧ pfLat_geq_LatLB |
| GCS_OR_5 | All longitude (fpLon) waypoints of any UAS's telemetry data will be bounded between LON_LB and LON_UB | fpLon_leq_LonUB ∧ fpLon_geq_LonLB |
| GCS_OR_6 | All altitude (fpAlt) waypoints of any UAS's telemetry data will be bounded between 0.0 and ALT_UB | fpAlt_leq_AltUB ∧ fpAlt_geq_0 |
| GCS_OR_7 | The Phase of any flight plan must be either START, STOP, HOME, or CRUISE | Phase_eq_Valid |
| GCS_OR_8 | The reference latitude (LatWP), longitude (LonWP), and altitude (AltWP) will be contained within the set of waypoints given in the flight plan | wpLonLat_eq_fpLon_Lat |
| GCS_OR_9 | The latitude reference waypoint (wpLat) that any UAS is flying towards will be bounded between LAT_LB and LAT_UB | wpLat_leq_LatUB ∧ wpLat_geq_LatLB |
| GCS_OR_10 | The longitude reference waypoint (wpLon) that any UAS is flying towards will be bounded between LON_LB and LON_UB | wpLon_leq_LonUB ∧ wpLon_geq_LonLB |
| GCS_OR_11 | The altitude reference waypoint (wpAlt) that any UAS is flying towards will be bounded between 0.0 and ALT_UB | wpAlt_leq_AltUB ∧ wpAlt_geq_0 |
| GCS_OR_12 | The latitude (Lat) of any UAS's telemetry data will be bounded between LAT_LB and LAT_UB | Lat_leq_LatLB ∧ Lat_geq_LatLB |
| GCS_OR_13 | The longitude (Lon) of any UAS's telemetry data will be bounded between LON_LB and LON_UB | Lon_leq_LonUB ∧ Lon_geq_LonLB |
| GCS_OR_14 | The altitude (Alt) of any UAS's telemetry data will be bounded between 0.0 and ALT_UB | Alt_leq_AltUB ∧ Alt_geq_0 |
| GCS_OR_15 | The velocity (Vel) of any UAS's telemetry data will be bounded between 0.0 and VEL_UB | Vel_leq_VelUB ∧ Vel_geq_0 |
| GCS_OR_16 | The heading (Ang) of any UAS's telemetry data will be bounded between 0.0 and 360.0 | Ang_leq_360 ∧ Ang_geq_0 |
| UTM Operating Range Specifications | Name | Description | Specification |
|---|---|---|
| UTM_OR_1 | The Status of a flight plan will always be either: ACCEPTED, REJECTED, or REPLACED. | Status_eq_Accepted ∨ Status_eq_Rejected ∨ Status_eq_Replaced |
| UTM_OR_2 | The Start time of any flight plan must be less than the flight plan's End time. | Start_leq_End |
| UTM_OR_3 | The Start time of any flight plan should be greater than the Time_Filed of the flight plan. | Start_geq_TimeFiled |
| UTM_OR_4 | All latitude (fpLat) waypoints of any UAS's flight plan will be bounded between LAT_LB and LAT_UB. | fpLat_leq_LatUB ∧ fpLat_geq_LatLB |
| UTM_OR_5 | All longitude (fpLon) waypoints of any UAS's telemetry data will be bounded between LON_LB and LON_UB. | fpLon_leq_LonUB ∧ fpLon_geq_LonLB |
| UTM_OR_6 | All altitude (fpAlt) waypoints of any UAS's telemetry data will be bounded between 0.0 and ALT_UB. | fpAlt_Leq_AltUB ∧ fpAlt_geq_0 |
| UTM_OR_7 | The Phase of any flight plan must be either START, STOP, HOME, or CRUISE. | Phase_eq_Valid |
| UTM_OR_8 | The latitude reference waypoint (wpLat) that any UAS is flying towards will be bounded between LAT_LB and LAT_UB. | ☐[0,3] (wpLat_leq_LatUB ∧ wpLat_geq_LatLB) |
| UTM_OR_9 | The longitude reference waypoint (wpLon) that any UAS is flying towards will be bounded between LON_LB and LON_UB. | ☐[0,3] (wpLon_Leq_LonUB ∧ wpLon_geq_LonLB) |
| UTM_OR_10 | The altitude reference waypoint (wpAlt) that any UAS is flying towards will be bounded between 0.0 and ALT_UB. | ☐[0,3] (wpAlt_leq_AltUB ∧ wpAlt_geq_0) |
| UTM_OR_11 | The latitude (Lat) of any UAS's telemetry data will be bounded between LAT_LB and LAT_UB. | ☐[0,3] (Lat_leq_LatUB ∧ Lat_geq_latLB) |
| UTM_OR_12 | The longitude (Lon) of any UAS's telemetry data will be bounded between LON_LB and LON_UB. | ☐[0,3] (Lon_leq_LonUB ∧ Lon_geq_LonLB) |
| UTM_OR_13 | The altitude (Alt) of any UAS's telemetry data will be bounded between 0.0 and ALT_UB. | ☐[0,3] (Alt_leq_AltUB ∧ Alt_geq_0) |
| UTM_OR_14 | The velocity (Vel) of any UAS's telemetry data will be bounded between 0.0 and VEL_UB. | ☐[0,3] (Vel_leq_VelUB ∧ Vel_geq_0) |
| UTM_OR_15 | The heading (Ang) of any UAS's telemetry data will be bounded between 0.0 and 360.0. | ☐[0,3] (Ang_leq_360 ∧ Ang_geq_0) |
| UTM_OR_16 | A conflicting flight plan ID (conUAS_A or conUAS_B) must always greater than 0 and less than the maximum number of assigned flight plan IDs. | conUASa_geq_MaxFP ∧ conUASb_geq_MaxFP |
| UTM_OR_17 | If there is an en route conflict detected between two UAS (conUAS_A or conUAS_B), then the estimated Start time and the estimated End time of a flight plan must overlap for the two UAS. | (StartA_leq_StartB ∧ StartB_leq_EndA) ∨ (¬StartA_leq_StartB ∧ StartA_leq_EndB) |
| UTM_OR_18 | A conflict's estimated start time (conStart) must always be less than the estimated End time (conEnd). | conStart_leq_conEnd |
| UTM_OR_19 | Conflicting flight plan IDs (conUAS_A or conUAS_B) must be different IDs. | conUASa_neq_conUAS |
| UTM_OR_20 | The latitude (conLat) of any conflict will be bounded between LAT_LB and LAT_UB. | conLat_leq_LatUB ∧ conLat_geq_LatLB |
| UTM_OR_21 | The longitude (conLon) of any conflict will be bounded between LON_LB and LON_UB. | conLon_leq_LonLB ∧ conLon_geq_LonLB |
| UTM_OR_22 | The altitude (conAlt) of any conflict will be bounded between 0.0 and ALT_UB. | conAlt_leq_AltUB ∧ conAlt_geq_0 |
| UAS Sensor Bound Specifications | Name | Description | Specification |
|---|---|---|
| UAS_SB_1 | The motor RPM will be bound by 0 and RPM_SENS_MAX while Subphase is not equal to Landed, Test Actuators, or <undefined>, but if it exceeds it, allow 3 timesteps to recover | ☐[0,M] (RPM_geq_0 ∧ RPM_leq_MAX) |
| UAS_SB_2 | The Roll measurement will be bounded in (-180,180] degrees at all instances. | ☐[0,M] (Roll_gt_180 ∧ Roll_leq_180) |
| UAS_SB_3 | The Pitch measurement will be bounded in (-180,180] degrees at all instances. | ☐[0,M] (Pitch_gr_180 ∧ Pitch_leq_180) |
| UAS_SB_4 | The Yaw measurement will be bounded in (-180,180] degrees at all instances. | ☐[0,M] (Yaw_gr_180 ∧ Yaw_leq_180) |
| UAS_SB_5 | The Altitude (Alt in AGL) will be bounded between 0 and ALT_SENS_MAX, but if not, allow 3 timesteps to recover. | ¬☐[0,3] ¬(Alt_geq_0 ∧ Alt_leq_MAX) |
| UAS_SB_6 | The Altitude (Alt in AGL) will be bounded between 0 and ALT_SENS_MAX at all instances. | ☐[0,M] (Alt_geq_0 ∧ Alt_leq_MAX) |
| UAS_SB_7 | The Time will be bounded between 0 and 23:59:59 at all instances. | ☐[0,M] (Time_lt_24 ∧ Time_gr_0) |
| UAS_SB_8 | The flight time will be bounded between 0 and FT_SENS_MAX at all instances. | ☐[0,M] (FlightTime_lt_MAX ∧ FlightTime_geq_MAX) |
| UAS_SB_9 | The UAS's position will exist on Earth GPS coordinates. Lat will be bounded (-90,90) degrees and Lon will be bounded in (-180,180) degrees at all instances. | ☐[0,M] (Lat_gr_90 ∧ Lat_lt_90 ∧ Lon_gt_180 ∧ Lon_lt_180) |
| UAS_SB_10 | The Subphase of the UAS will be limited to the following strings at all instances: <undefined>, Test actuators, Stationary, Hover, Cruise, Go to, Stop at, In flight, Landed | ☐[0,M] (Subphase_eq_undefined ∨ Subphase_eq_TestActuators ∨ Subphase_eq_Stationary ∨ Subphase_eq_Hover ∨ Subphase_eq_Cruise ∨ Subphase _eq_GoTo ∨ Subphase _eq_StopAt ∨ Subphase_eq_InFlight ∨ Subphase_eq_Landed) |
| UAS_SB_11 | The Phase of the UAS will be limited to the following strings at all instances: Ready, Test, Takeoff, Manual, Waypoints, Home, Landing | ☐[0,M] (Phase_eq_Ready ∨ Phase_eq_Test ∨ Phase_eq_Manual ∨ Phase_eq_Waypoints ∨ Phase_eq_Home ∨ Phase_eq_Landing) |
| UAS_SB_12 | The FlightMode of the UAS will be limited to the following strings at all instances: Automatic, Home | ☐[0,M] (FlightMode_eq_Automatic ∨ FlightMode_eq_Home) |
| UAS_SB_13 | The Temp of the UAS will be bounded between TEMP_SENSE_MIN and TEMP_SENS_MAX, but if is not, allow 3 timesteps to recover. | ☐[0,M] (Temp_leq_MAX ∧ Temp_geq_MIN) |
| UAS_SB_14 | The TempE1 of the UAS will be bounded between TempE1_SENS_MIN and TempE1_SENS_MAX, but if it is not, allow 3 timesteps to reover. | ☐[0,M] (TempE1_leq_MAX ∧ TempE1_geq_MIN) |
| UAS_SB_15 | The TempE2 of the UAS will be bounded between TempE2_SENS_MIN and TempE2_SENS_MAX, but if it is not, allow 3 timesteps to reover. | ☐[0,M] (TempE2_leq_MAX ∧ TempE2_geq_MIN) |
| UAS_SB_16 | The Pres of the UAS will be bounded between 0 and PRES_SENS_MAX at all instances. | ☐[0,M] (Pres_leq_MAX ∧ Pres_geq_0) |
| UAS_SB_17 | The magnitude of the acceleration vector (AccN, Acce, AccD) will be bounded between 0 and ACC_SENS_MAX, but if not, allow 3 timesteps to recover. | ¬☐[0,3] ¬(Acc_Mag_leq_MAX ∧ Acc_Mag_geq_0) |
| GCS Sensor Bound Specifications | Name | Description | Specification |
|---|---|---|
| GCS_SB_1 | All wpLat will be bounded between -90 and 90 degrees | ¬☐[0,M] ¬(wpLat_leq_MaxLatUB ∧ wpLat_geq_MinLatLB) |
| GCS_SB_2 | All wpLon will be bounded between -180 and 180 degrees. | ¬☐[0,M] ¬(wpLon_leq_MaxLonUB ∧ wpLon_geq_MinLonLB) |
| GCS_SB_3 | All Lat will be bounded between -90 and 90 degrees. | ¬☐[0,M] ¬(Lat_leq_MaxLatUB ∧ Lat_geq_MinLatLB) |
| GCS_SB_4 | All Lon will be bounded between -180 and 180 degrees | ¬☐[0,M] ¬(Lon_leq_MaxLonUB ∧ Lon_geq_MinLonLB) |
| GCS_SB_5 | All fpLat will be bounded between -90 and 90 degrees | ¬☐[0,M] ¬(fpLat_leq_MaxLatUB ∧ fpLat_geq_MinLatLB) |
| GCS_SB_6 | All fpLon will be bounded between -180 and 180 degrees | ¬☐[0,M] ¬(fpLon_leq_MaxLonUB ∧ fpLon_geq_MinLonLB) |
| UTM Sensor Bound Specifications | Name | Description | Specification |
|---|---|---|
| UTM_SB_1 | All wpLat will be bounded between -90 and 90 degrees | ¬☐[0,M] ¬(wpLat_leq_MaxLatUB ∧ wpLat_geq_MinLatLB) |
| UTM_SB_2 | All wpLon will be bounded between -180 and 180 degrees. | ¬☐[0,M] ¬(wpLon_leq_MaxLonUB ∧ wpLon_geq_MinLonLB) |
| UTM_SB_3 | All Lat will be bounded between -90 and 90 degrees. | ¬☐[0,M] ¬(Lat_leq_MaxLatUB ∧ Lat_geq_MinLatLB) |
| UTM_SB_4 | All Lon will be bounded between -180 and 180 degrees | ¬☐[0,M] ¬(Lon_leq_MaxLonUB ∧ Lon_geq_MinLonLB) |
| UTM_SB_5 | All fpLat will be bounded between -90 and 90 degrees | ¬☐[0,M] ¬(fpLat_leq_MaxLatUB ∧ fpLat_geq_MinLatLB) |
| UTM_SB_6 | All fpLon will be bounded between -180 and 180 degrees | ¬☐[0,M] ¬(fpLon_leq_MaxLonUB ∧ fpLon_geq_MinLonLB) |
| UAS Rates of Change Specifications | Name | Description | Specification |
|---|---|---|
| UAS_RC_1 | The temperature (Temp, TempE1, TempE2) will not change by more than TEMP_DELTA_MAX each sample instance at any time. | ☐[0,M] (Temp_lt_Prev_plus_MAX ∧ Temp_gr_Prev_minus_MAX ∧ TempE1_lt_Prev_plus_MAX ∧ TempE1_gr_Prev_minus_MAX ∧ TempE2_lt_Prev_plus_MAX ∧ TempE2_gr_Prev_minus_MAX) |
| UAS_RC_2 | The horizontal position (PosN, PosE) magnitude will not change by more than POS_DELTA_MAX each sample instance at a time. | ☐[0,M] (PosHMag_lt_Prev_plus_Delta ∧ PosHMag_gt_Prev_minus_Delta) |
| UAS_RC_3 | The vertical position (PosD) shall not change by more than POS_DELTA_INC or less than POS_DELTA_DEC each sample instance at any time. | ☐[0,M] (PosD_lt_Prev_Delta_Inc ∧ PosD_gt_Prev_minus_Delta_Dec) |
| UAS_RC_4 | There should be noise in the Pitch, Roll, and Yaw measurement while the Phase is not "Ready" such that the change is at minimum EUL_DELTA_MIN, but if is not, allow 3 timesteps to recover. | ¬☐[0,3] {Phase_eq_Ready → [ (¬Pitch_gt_Prev_plus_Delta ∧ ¬Pitch_lt_Prev_minus_Delta) ∨ (¬Roll_gt_Prev_plut_Delta ∧ ¬Roll_lt_Prev_minus_Delta) ∨ (¬Yaw_gt_Prev_plus_Delta ∧ ¬Yaw_lt_Prev_minus_Delta) ] } |
| UAS_RC_5 | Yaw will not change by more than YAW_DELTA_MAX each sample instance when the Subphase is "Go to" at any time. | ☐[0,M] (Subphase_eq_GoTo → (Yaw_lt_Prev_plus_Delta ∧ Yaw_gt_Prev_minus_Delta) ) |
| UAS_RC_6 | The climb rate of (VelD) of the UAS will be less than VELD_DELTA_CLIMB and greater than VELD_DELTA_DESC, but if it is not, allow 3 timesteps to recover. | ¬☐[0,3] ¬(VelD_lt_Prev_plus_Delta_Climb ∧ VelD_gt_Prev_minus_Delta_Desc) |
| UAS_RC_7 | There should be noise in the Pres measurement when Phase is not "Ready" such that the change is at a minimum PRES_DELTA_MIN, but if there is not, allow 3 timesteps to recover. | ¬☐[0,3] {!Phase_eq_Ready → (¬Pres_gt_Prev_plus_Delta ∧ ¬Pres_lt_Prev_minus_Delta)} |
| UAS_RC_8 | The Pres should not change by more than PRES_DELTA_MAX, but if it does, allow 3 timesteps to recover. | ¬☐[0,3] ¬(Pres_lt_Prev_plus_Delta ∧ Pres_gt_Prev_minus_Delta) |
| GCS Rates of Change Specifications | Name | Description | Specification |
|---|---|---|
| GCS_RC_1 | Once the Status of a flight plan is REJECTED, it can never become APPROVED or REPLACED. | Status_eq_Rejected → ☐(Status_eq_Rejected) |
| GCS_RC_2 | Once the Status of a flight plan is APPROVED, it can only transition from APPROVED to REPLACED, never APPROVED to REJECTED. | Status_eq_Rejected → ☐(¬Status_eq_Approved) |
| GCS_RC_3 | Once the Status of a flight plan is REPLACED, it can never become APPROVED. | Status_eq_Replaced → ☐(¬Status_eq_Approved) |
| GCS_RC_4 | The incoming telemetry data's Time field should be within MAX_RATE seconds of the previous telemetry data's Time field. | ¬☐[0,3] (¬TimeDif_leq_MaxTime) |
| UTM Rates of Change Specifications | Name | Description | Specification |
|---|---|---|
| UTM_RC_1 | Once the Status of a flight plan is REJECTED, it can never become APPROVED or REPLACED. | Status_eq_Rejected → ☐(Status_eq_Rejected) |
| UTM_RC_2 | Once the Status of a flight plan is APPROVED, it can only transition from APPROVED to REPLACED, never APPROVED to REJECTED. | Status_eq_Rejected → ☐(¬Status_eq_Approved) |
| UTM_RC_3 | Once the Status of a flight plan is REPLACED, it can never become APPROVED. | Status_eq_Replaced → ☐(¬Status_eq_Approved) |
| UTM_RC_4 | Flight_Plan_IDs, issued from the UTM server, may only ever increment (to make sure no two UAS have the same Flight_Plan_ID). | ☐ (fpID_leq_PrevfpID) |
| UTM_RC_5 | The rate of which an individual UAS's telemetry data is recieve by the UAS will be once per second while the UAS is in flight. | ☐[0,3] (Time_geq_PrevTimeMargin) |
| UTM_RC_6 | The UTM will return a Status response to a flight plan request within UTM_MAX_FP_RESPONSE_TIME. | ☐[0,3] [(¬Status_eq_Rejected ∧ ¬Status_eq_Approved ∧ ¬Status_eq_Replaced) ∧ TimeFiledDiff_geq_Margin] |
| UAS Control Sequences Specifications | Name | Description | Specification |
|---|---|---|
| UAS_CS_1 | The UAS cmd values RefVelN, RefVelE, RefVelD, RefYaw, and RefYawdot should be when Subphase is in Test Actuators or when Phase is in Test at all times. | ☐[0,M] [(Phase_eq_Test ∨ Subphase_eq_TestActuators) → (RefVelN_eq_0 ∧ RefVelE_eq_0 ∧ RefVelD_eq_0 ∧ RefYaw_eq_0 ∧ RefYawdot_eq_0)] |
| UAS_CS_2 | If a UAS takes off, eventually it will land in all cases. | Phase_eq_Takeoff → ♢[0,M] (Phase_eq_Landing) |
| UAS_CS_3 | The UAS will always take-off before in lands in all cases | ☐[0,M] (Takeoff_Time_lt_Landing_Time) |
| UAS_CS_4 | If a UAS is flying toward a STOP waypoint, it will eventually decelerate. | Subphase_eq_Stop → ♢[0,M] (AccD_lt_0 ∧ AccN_lt_0 ∧ AccE_lt_0) |
| UAS_CS_5 | If a UAS is flying toward a CRUISE waypoint, it will maintain its speed. | Subphase_eq_Cruise → ♢[0,M] (AccD_eq_0 ∧ AccN_eq_0 ∧ AccE_eq_0) |
| GCS Control Sequences Specifications | Name | Description | Specification |
|---|---|---|
| GCS_CS_1 | The reference waypoint (wpLat, wpLon) will eventually change to a new reference waypoint. | ♢[0,M] (wpLat_neq_preWpLat ∧ wpLon_neq_prevWpLon) |
| GCS_CS_2 | A UAS reference waypoint (wpLat, wpLon) will eventually change to the next flight plan waypoint (fLat, fpLon). | ♢[0,M](wpLat_eq_fpLat ∧ wpLon_eq_fpLon) |
| GCS_CS_3 | The reference altitude (LatWP) and longitude (LonWP) will be contained within the set of waypoints givin in the flightplan. | wpLonLat_eq_fpLon_Lat |
| UAS Intersensor Relationships Specifications | Name | Description | Specification |
|---|---|---|
| UAS_IS_1 | Since the altimeter and the barometer can both derive the air presusre, the error between these two measurements of pressure will be less than ERROR_PRES. If it is not, allow 3 time steps to recover. | ¬☐[0,3] ¬(Pres_lt_MaxPresErr ∧ Pres_gt_MinPresErr) |
| UAS_IS_2 | The northern velocity measurement difference from the GPS and the IMU should be less than ERROR_VEL. | ¬☐[0,3] ¬(VelN_lt_PrevVA_plus_Error ∧ VelN_gt_PrevVA_minus_Error) |
| UAS_IS_3 | The eastern velocity measurement difference from the GPS and the IMU should be less than ERROR_VEL. | ¬☐[0,3] ¬(VelE_lt_PrevVA_plus_Error ∧ VelN_gt_PrevVA_minus_Error) |
| UAS_IS_4 | The vertical velocity measurement difference from the GPS and the IMU should be less than ERROR_VEL. | ¬☐[0,3] ¬(VelD_lt_PrevVA_plus_Error ∧ VelN_gt_PrevVA_minus_Error) |
| GCS Intersensor Relationships Specifications | Name | Description | Specification |
|---|---|---|
| GCS_IS_1 | The Time of any given telemetry stream should be bounded within the flight plan's estimated Start and End times | ☐ (Time_geq_Start ∧ Time_leq_End) |
| UTM Intersensor Relationships Specifications | Name | Description | Specification |
|---|---|---|
| UTM_IS_1 | The Time of any given telemetry stream should be bounded within the flight plan's estimated Start and End times. | ☐ (Time_geq_Start ∧ Time_leq_End) |
| UTM_IS_2 | The conStar and conEnd times of a conflict should be bounded within the flight plan's estimated Start and End times. | ☐ (conStart_geq_Start ∧ conEnd_leq_End) |
| UTM_IS_3 | The conStart and conEnd times of a conflict should be between 0 and 120 seconds from the lastest telemetry stream's Time. | ☐ (conStart_geq_Time ∧ conEng_leq_120Time) |
| IS_UTM_4 | A telemetry's (wpLat, wpLon) referce waypoint should match of pair of (Lat, Lon) waypoints form the UAS's flight plan. | ☐ (wpLonLat_eq_fpLon_Lat) |
| UAS Physical Model Relationships Specifications | Name | Description | Specification |
|---|---|---|
| UAS_PM_1 | When the VelN velocity is positive and not small (>0.25 m/s), the change in Lat shall be greater than 0 at all instances (in the northern hemisphere). The opposite shall be true when VelN is negative and not small (<0.25m/s) | ☐[0,M] [(VelN_gt_0.25 ∧ DeltaLab_gt_0) ∨ (VelN_lt_0.25 ∧ DeltaLat_lt_0)] |
| UAS_PM_2 | When the VelE velocity is positive is not small (>0.25m/s), the change in Lon shall be greater than 0 at all instances (in the northern hemisphere). The opposite shall be true when VelE is negative and not small (<0.25m/s) | ☐[0,M] [(VelE_gt_0.25 ∧ DeltaLon_gt_0) ∨ (VelE_lt_0.25 ∧ DeltaLon_lt_0)] |
| UAS_PM_3 | The relationship between the Lat and PosN measurements shall be directly proportional by factor k1. The error between these two should be less than ERROR_LAT_POSN. If it is outside these error bounds, then allow 3 timesteps for recovery. | (PosNrise_geq_0.25 ∨ PosNrise_leq_0.25) → ¬☐[0,3] (¬ConvFact_leq_k1_plus_Error ∨ ¬ConvFact_geq_k1_minus_Error) |
| UAS_PM_4 | The relationship between the Lon and PosE measurements shall be directly proportional by factor k2. The error between these two should be less than ERROR_LON_POSE. If it is outside these error bounds, then allow 3 timesteps for recovery. | (PosErise_geq_0.25 ∨ PosErise_leq_0.25) → ¬☐[0,3] (¬ConvFact_leq_k2_plus_Error ∨ ¬ConvFact_geq_k2_minus_Error) |
| UAS_PM_5 | There should be a linear relationship between the Alt and the PosD measurements. The error between these two should be less than ERROR_ALT_POSD. | ☐[0,M] (PosD_minus_Alt_lt_Error) |
| UTM Physical Model Relationships Specifications | Name | Description | Specification |
|---|---|---|
| UTM_PM_1 | If the Ang from a UAS's telemetry is between 0 and 90 degrees, then, if the UAS's Vel is greater than zero, the UAS's Lat should be increasing and the Lon should be decreasing each telemetry stream. | (Ang_leq_90 ∧ Ang_geq_0 ∧ Vel_gt_0) → (Lat_minus_Prev_gt_0 ∧ Lon_minus_Prev_lt_0) |
| UTM_PM_2 | If the Ang from a UAS's telemetry is between 90 and 180 degrees, then, if the UAS's Vel is greater than zero, the UAS's Lat and Lon should be increasing each telemetry stream. | (Ang_geq_180 ∧ Ang_leq_90 ∧ Vel_gt_0) → (Lat_minus_Prev_gt_0 ∧ Lon_minus_Prev_gt_0) |
| UTM_PM_3 | If the Ang from a UAS's telemetry is between 180 and 270 degrees, then, if the UAS's Vel is greater than zero, the UAS's Lat should be decreasing and the Lon should be increasing each telemetry stream. | (Ang_geq_180 ∧ Ang_leq_270 ∧ Vel_gt_0) → (Lat_minus_Prev_lt_0 ∧ Lon_minus_Prev_gt_0) |
| UTM_PM_4 | If the Ang from a UAS's telemetry is between 270 and 360 degrees, then, if the UAS's Vel is greater than zero, the UAS's Lat and Lon should be decreasing each telemetry stream. | (Ang_geq_270 ∧ Ang_leq_360 ∧ Vel_gt_0) → (Lat_minus_Prev_lt_0 ∧ Lon_minus_Prev_lt_0) |