Verifying Safety of Behaviour Trees in Event-B
This work addresses safety verification for robots in critical environments, but it is incremental as it builds on existing BT formalization methods.
The authors tackled the problem of verifying safety and reliability of Behavior Trees (BTs) used in robotics, proposing a formal specification and methodology to prove invariants while keeping complexity low for users, enabling testing without deep formalization knowledge.
Behavior Trees (BT) are becoming increasingly popular in the robotics community. The BT tool is well suited for decision-making applications allowing a robot to perform complex behavior while being explainable to humans as well. Verifying that BTs used are well constructed with respect to safety and reliability requirements is essential, especially for robots operating in critical environments. In this work, we propose a formal specification of Behavior Trees and a methodology to prove invariants of already used trees, while keeping the complexity of the formalization of the tree simple for the final user. Allowing the possibility to test the particular instance of the behavior tree without the necessity to know the more abstract levels of the formalization.