Lecture
From Natural Language to Safe Actuation: A Formally Verified Shield for LLM-Driven Drone Allocation
- at -
- Hall C6C6.501
- Language: English
- Type: Lecture
Lecture description
Large language models let warehouse operators dispatch and re-task an autonomous drone fleet in plain natural language — but their probabilistic, opaque behaviour makes them unsafe to wire directly into actuation. We present a drone allocation system for warehouse monitoring and inventory in which a compact, quantised LLM, running on-device with llama.cpp, parses natural-language instructions into structured allocation commands. Between the LLM's structured output and the allocation logic we insert a \textit{shield}: a lightweight runtime enforcement layer that passes safe commands through unchanged and corrects or rejects any command that would drive the system into an unsafe state. The central question we answer is how to trust the shield itself. We build an abstraction of the allocation system in Rebeca, an actor-based modelling language with model-checking support, express the system's safety and consistency requirements as assertions, and use model checking to verify they hold for any command sequence — including the unsafe output an LLM can produce. Verified properties include: every command references an existing drone and an in-bounds location; at most one drone is ever assigned to a given aisle (collision avoidance); no drone holds more than one active mission; a drone is dispatched only if its remaining charge covers the mission plus a return-to-dock reserve; and the allocator is deadlock-free, so no pending task is blocked indefinitely. The shield is then constructed to enforce these assertions by design, decoupling the safety case from the unverifiable internals of the model. We deploy the complete pipeline — llama.cpp parser, shield, and allocation system — on an STM32MP257F (dual Arm Cortex-A35) running embedded Linux, demonstrating that formal, functional-safety-grade assurance for on-device LLM control is achievable within the resource budget of real industrial hardware.
