Automation of Test Case Generation from Behavior Tree Requirements Models

Behavior Trees (BTs) are a graphical notation for requirements capture that is easier to read than other formal notations, with direct traceability between individual functional requirements and their representation in the BT model. This paper investigates whether this relationship can be extended to generation of test cases, using a symbolic model checker to ensure correctness and completeness of test cases with respect to the model. To do so it was necessary to provide mechanisms for test planner input and to control the combinatorial explosion of test cases that results from models containing parallel behaviour. The result is an automated process for generating a complete set of natural-language test cases, with tracing back to the original requirements and with correctness and completeness guaranteed by the model checker. The approach is demonstrated on an Automated Teller Machine example and then applied to an example from air traffic control in a model with multi-threaded behaviour.