Automatic protocol conformance checking of recursive and parallel component-based systems

Abstract

Today model checking of security or safety properties of component-based systems based on finite protocols has the flaw that either parallel or sequential systems can be checked. Parallel systems can be described often by well known Petri nets, but it is not possible to model recursive behaviour. On the other hand sequential systems based on pushdown automata can capture recursion and recursive callbacks [27], but they do not provide parallel behaviour in general. In this work we show how this gap can be filled if process rewrite systems (introduced by Mayr [16]) are used to capture the behaviour of components. The protocols of the components interfaces specified as finite state machines can be combined to a system equal to a process rewrite system. By calculating the reachability of the fault state range one gets a trace (counterexample) which does not satisfy the properties specified by all protocols of the combined components, if any error exists. © 2008 Springer.