Tool-assisted verification of behaviour networks

This paper deals with the problem of assisting developers when verifying properties of complex behaviour-based systems. A central aspect of behaviour-based systems is the interaction between the behaviours, as a lot of the functionality of a system typically arises from this interaction. Hence, verification has to deal with the specialities of behaviour interaction. Previous work has introduced a concept for modelling behaviour-based systems as networks of finite-state automata and for applying model checking as verification technique. As the manual verification of large networks is tedious and errorprone, the work at hand introduces a concept for assisting developers by partly automating the verification process. The applicability of the presented approach is demonstrated using the behaviour-based control system of an autonomous bucket excavator.