Quantitative Aspects of Behaviour Network Verification

摘要

This paper presents quantitative aspects of an approach for the modelling and verification of behaviour networks published previously and describes the application of said modelling technique to a complex coordinating behaviour. In order to decrease the number of interconnection failures in behaviour networks, verification techniques focusing on behaviour interaction can be applied. In previous work, the authors have introduced a novel approach for modelling behaviour networks as networks of finite-state automata, to which model checking can be applied as verification technique. This paper presents how the approach can be used to model complex behaviours and provides calculations of the numbers of states, transitions, and state variables in the resulting automata.