Quantitative Aspects of Behaviour Network Verification

Abstract. This paper presents quantitative aspects of an approach for the modelling and verication 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, verication 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 nite-state automata, to which model checking can be applied as verication 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.