Analysis of Dynamic Communicating Systems by Hierarchical Abstraction

Authors Jörg Bauer, Reinhard Wilhelm

Thumbnail PDF


  • Filesize: 0.72 MB
  • 25 pages

Document Identifiers

Author Details

Jörg Bauer
Reinhard Wilhelm

Cite AsGet BibTex

Jörg Bauer and Reinhard Wilhelm. Analysis of Dynamic Communicating Systems by Hierarchical Abstraction. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


We propose a new abstraction technique for verifying topology properties of dynamic communicating systems (DCS), a special class of infinite-state systems. DCS are characterized by unbounded creation and destruction of objects along with an evolving communication connectivity or topology. We employ a lightweight graph transformation system to specify DCS. Hierarchical Abstraction (HA) computes a bounded over-approximation of all topologies that can occur in a DCS directly from its transformation rules. HA works in two steps. First, for each connected component, called cluster, of a topology, objects sharing a common property are summarized to one abstract object. Then isomorphic abstract connected components are summarized to one abstract component, called abstract cluster. This yields a conservative approximation of all graphs that may occur during any DCS run. The technique is implemented.
  • Graph transformation
  • Abstract Interpretation
  • Shape Analysis


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads