Symbolic verification and test generation for a network of communicating FSMs

Abstract

A network of communicating FSMs (NCFSMs) is a useful formalism to model complex concurrent systems, but its use demands efficient analysis algorithms. We propose a new symbolic framework for NCFMS verification and test generation. We explore the use of the breadth-first search (BFS) and saturation algorithms to compute the "unstable transitive closure" of transitions for the observable product machine of an NCFSM. Our framework can verify properties such as livelock freeness and includes a fully automatic test generation based on mutation analysis. Being symbolic, our framework can efficiently manage a large number of mutants with moderate resource consumption and derive a test suite to distinguish all non-equivalent first-order mutants. © 2011 Springer-Verlag.