🤓 Latest Submissions
BobGuard: Agentic UAV Failsafe Verification
UAV failsafe software must behave correctly when failures such as communication loss, GPS loss, and critical battery conditions occur individually or simultaneously. In practice, these interactions can create unsafe state transitions that are difficult to detect through manual testing alone. A system may correctly handle each failure in isolation yet behave incorrectly when failures occur in a different order or overlap. BobGuard is a software-only UAV failsafe verification framework built with IBM Bob. It models UAV behavior as a state machine with NORMAL, LOITER, RETURN_HOME, LAND, and TERMINATED states, then verifies that the implementation complies with explicitly defined safety requirements. BobGuard automatically generates individual, sequential, and combined failure scenarios, records complete state-transition traces, detects safety violations, classifies their severity, and produces human-readable verification reports. It also performs regression testing and mutation testing to validate whether the verification framework can detect newly introduced defects rather than simply pass a known-good implementation. Example failures include communication loss while airborne, GPS loss during Return-to-Home, critical battery while loitering, conflicting recovery conditions, and multi-failure event sequences. BobGuard also distinguishes genuine safety violations from expected operational contingency states such as LOITER while an active failure remains. The target users are robotics and autonomous-systems developers who need a repeatable way to inspect and validate failsafe logic before integration with real hardware or higher-fidelity simulators. Users provide or modify a failsafe state machine, execute the BobGuard verification workflow, and review scenario results, transition traces, detected violations, and recommended fixes. The current prototype verified 61 requirement-based scenarios with 61/61 passing after refinement, 0 CRITICAL violations, and 0 HIGH violations. Mutation testing injected five realistic defect classes, and BobGuard detected all 5/5 for a 100% mutation detection rate. What makes BobGuard different is that IBM Bob is used not only to generate code, but across the verification lifecycle: implementation analysis, defect diagnosis, targeted repair, edge-case discovery, requirement refinement, regression testing, mutation testing, reporting, and release validation. This turns manual UAV failsafe debugging into a repeatable agentic software-verification workflow.
27 Sep 2026
