Inter-agent Data Flow Analysis of Abstract State Machines

This paper introduces an approach to apply data flow testing techniques to multi-agent abstract state machines. In particular, we analyze the different types of functions in ASMs and deal with the problem of functions that are monitored by a given agent but controlled by another one, functions that are shared between several agents, and derived functions. We revise the concepts of function definition, use in predicate, and use in computation accordingly, and show how definition-use paths are specified in these cases. Finally, we propose a model-checking based approach to derive automatically test cases satisfying a given set of data flow coverage criteria.