Communication Topology Analysis for Concurrent Programs

Abstract. In this article, we address the problem of statically determining an approximation of the communication topology of concurrent programs. These programs may contain dynamic process and channel creations and may communicate channel names as well as functions, possibly containing other communications. We introduce a control ow analysis which builds nite state automata to improve its precision. The method is twofold. First, we build an automaton for each process in the concurrent system yielding an approximation of how the synchronizations realized by the sequential components are ordered. Second, we extract the communication topology from a reduced product automaton, which size is polynomial in the size of the original program. This analysis was implemented and we apply it to the veri cation of a circuit allocation mechanism.

• Type: Conference
• Year: 2000
• Where: SPIN
• Authors: Matthieu Martel, Marc Gengler
• Keywords: Communication Topology, Control Ow Analysis, Nite State Automata, SPIN 2000, Theoretical Computer Science