Slicing Behavior Trees for verification of large systems

It is essential to ensure the correctness of software systems, especially for large and safety-critical applications. Detecting problems earlier in the software cycle, such as in the specification and design phases, would significantly reduce the costs involved. Rigorous automated approaches are ideal for detecting such problems. Model checking is an automated verification technique which exhaustively searches the state space to determine whether a model of the system satisfies a given property. How-ever, model checking suffers from state explosion, preventing large systems from being verified. The Behavior Tree specification language enables engineers to handle the complexity of large systems, by allowing them to focus on one requirement at a time. Behavior Trees maintain strong links to the original requirements of the system. There has been support for automatic translation of Behavior Trees into model checking languages. However, due to the state explosion problem, large Behavior Trees still cannot be verified. Program slicing is a reduction technique which automatically removes irrelevant portions of the program, usually applied for improving understanding and debugging. In this thesis, a technique for reducing Behavior Trees prior to verification is proposed, based on the concepts of program slicing