Hardware-in-the-Loop Validation of Formal Models: an Application to AI-Controlled Drones

This work presents a hardware-in-the-loop technique that enables a formal model to be connected directly to an external system. Thus, one can run and validate the formal model in a controlled and realistic environment. We implement the technique inside ProB via a new JSON-RPC communication library, along with new debugging features. Furthermore, we demonstrate the technique on drones, for which we (1) create a formal B model of safe drone movements, (2) train and use a reinforcement learning agent as an action planner, and (3) employ the B model as a safety shield. In this context, we analyze the challenges posed by the gap between the formal model and the real world. This workflow was successfully employed in two iterations of a master-level course as individual student projects. Our hardware-in-the-loop technique enables interactive control of the external drone system through animation or autonomous control through simulation. For debugging purposes, one can employ the existing debugging and visualization features of the ProB toolchain. Further, we developed a novel feature that links model states and executed actions with a video recording. The feature is useful for postmortem inspection of failed validation runs (e.g., drone crashes).