Reference:

J. Bauer, Tobe Toben, and Bernd Westphal. Mind the shapes: Abstraction refinement via topology invariants. In Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura, editors, Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings, volume 4762, pages 35–50. Springer, 2007.

Abstract:

Dynamic Communication Systems (DCS) are infinite state systems where an unbounded number of processes operate in an evolving communication topology. For automated verification of properties of DCS, finitary abstractions based on exploiting symmetry can be employed. However, these abstractions give rise to spurious behaviour that often inhibits to successfully prove relevant properties. In this paper, we propose to combine a particular finitary abstraction with global system invariants obtained by abstract interpretation. These system invariants establish an over-approximation of possible communication topologies occurring at runtime, which can be used to identify and exclude spurious behaviour introduced by the finitary abstraction, which is thereby refined. Based on a running example of car platooning, we demonstrate that our approach allows to verify temporal DCS properties that no technique in isolation is able to prove.

Keywords:

dynamic communication systems, graph grammar verification, model checking, tool chain

Suggested BibTeX entry:

@inproceedings{BauerTW07,
    author = {J. Bauer and Tobe Toben and Bernd Westphal},
    booktitle = {Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings},
    editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura},
    pages = {35-50},
    publisher = {Springer},
    title = {Mind the Shapes: Abstraction Refinement Via Topology Invariants},
    volume = {4762},
    year = {2007}
}