2000 | OriginalPaper | Buchkapitel
Communication Topology Analysis for Concurrent Programs
verfasst von : Matthieu Martel, Marc Gengler
Erschienen in: SPIN Model Checking and Software Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 flow analysis which builds finite 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 verification of a circuit allocation mechanism.