2026-07-24T10:08:49Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:727 2024-03-06T11:06:43Z ddc:004 open_access

Analysis of Dynamic Communicating Systems by Hierarchical Abstraction Bauer, Jörg Wilhelm, Reinhard Graph transformation Abstract Interpretation Shape Analysis 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jörg Bauer and Reinhard Wilhelm 2006 Is Part Of Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.06081.3 urn:nbn:de:0030-drops-7271 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.3 eng https://creativecommons.org/licenses/by/4.0/legalcode