Towards runtime verification of collaborative embedded systems

A group of collaborative embedded systems does not depend on a central authority to operate in uncertain environments. By engaging in various negotiation protocols, the participants assign roles, schedule tasks, and combine their world views for more resilient perception and planning. To verify functional correctness, critical components can be tested with simulation-based methods, but the possibility of runtime faults still necessitates online monitoring. In this work, we characterize and address the runtime verification problem in the context of collaborative embedded systems. We present a case study based on industrial transport robots and model the main operating procedure, a distributed bidding protocol. The key properties that must hold for functional correctness turn out to comprise multiple semantic concepts that cannot be jointly expressed with any single formalism. To address this issue, we identify three specification languages that are particularly suitable for monitoring of collaborative embedded systems: Certifying distributed algorithms, trace expressions, and real-valued temporal logic. We show how each of them can be used to capture a subset of the relevant properties and outline a way of integrating them into a common framework.