Formal modeling and verification of behavior trees using BIP framework
Qiang Wang, Simon Bliudze, Min Zhang, Huadong Dai, Yongxin Zhao
Presenter: TBA Session Chair: TBA
A formal modeling and verification method for behavior trees (BTs) is proposed. The method is based on a compositional model transformation of BTs into the formal component-based system design framework BIP (Behavior-Interaction-Priority). In the transformation, each BT node is encoded as an individual BIP component that is formally defined by an extended finite state automaton (FSA), and each BT edge is encoded as a set of interactions that describes the allowed coordination between components. The correctness of the model transformation is proven based on the formal semantics of BIP, and a prototype tool has been implemented that enables the automated verification of BTs. Two practical case studies show that the tool-chain can not only verify the correctness of BTs, but also detect the potential design flaws automatically.