BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//ical.marudot.com//iCal Event Maker
CALSCALE:GREGORIAN
BEGIN:VTIMEZONE
TZID:Europe/Berlin
LAST-MODIFIED:20260721T092906Z
TZURL:https://www.tzurl.org/zoneinfo-outlook/Europe/Berlin
X-LIC-LOCATION:Europe/Berlin
BEGIN:DAYLIGHT
TZNAME:CEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20261005T153935Z
UID:1791214657154-43022@ical.marudot.com
DTSTART;TZID=Europe/Berlin:20261113T112000
DTEND;TZID=Europe/Berlin:20261113T114000
SUMMARY:From Natural Language to Safe Actuation: A Formally Verified Shield for LLM-Driven Drone Allocation
URL:https://electronica.de/en/event-program/forums/lecture/from-natural-language-to-safe-actuation-a-formally-verified-shield-for-llm-driven-drone-allocation-17533/
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.
LOCATION:Embedded Developer Forum\, Hall C6\, Stand C6.501
BEGIN:VALARM
ACTION:DISPLAY
DESCRIPTION:From Natural Language to Safe Actuation: A Formally Verified Shield for LLM-Driven Drone Allocation
TRIGGER:-PT1H
END:VALARM
END:VEVENT
END:VCALENDAR