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. However, 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. The technique is shown to preserve all properties specified in the language CTL*-X, which is CTL* without the next operator. Thus, a property will be proved on the sliced model if and only if it is proved on the original model. The slicing approach is demonstrated on two case studies, producing significant reductions in verification time.
A new optimisation technique is also proposed, to allow the Behavior Tree to be reduced even further, by eliminating nodes which are infeasible. The technique is able to reduce slices more than previous approaches. The optimisation technique is also shown to preserve CTL*-X properties.
No other slicing method is able to preserve properties which contain the next operator. Another contribution of this thesis is a novel method for producing slices that are able to preserve full CTL*, including properties containing the next operator. This technique is shown to be correct by establishing a new form of branching bisimulation, known as Next-Preserving Branching Bisimulation. Weak forms of bisimulation are normally unable to preserve properties containing the next operator. Next-preserving branching bisimulation is shown to preserve full CTL*, which includes the next operator. The new form of bisimulation allows similar techniques to be developed for other modelling languages as well, since all that is required is to show the establishment of a next-preserving branching bisimulation.
The final outcome of the thesis is a slicing approach which can effectively reduce Behavior Trees, in order to allow large systems to be verified. Furthermore, the thesis gives useful theoretical results about property preservation of full CTL* by next-preserving branching bisimulation.