%0 Conference Proceedings %T Parameterized Verification of Track Topology Aggregation Protocols %+ Albert-Ludwigs-Universität Freiburg %A Feo-Arenis, Sergio %A Westphal, Bernd %Z Part 2: Session 1: Verification %< avec comité de lecture %( Lecture Notes in Computer Science %B 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE) %C Florence, Italy %Y Dirk Beyer %Y Michele Boreale %I Springer %3 Formal Techniques for Distributed Systems %V LNCS-7892 %P 35-49 %8 2013-06-03 %D 2013 %R 10.1007/978-3-642-38592-6_4 %Z Computer Science [cs] %Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers %X We present an approach for the verification aggregation protocols, which may be used to perform critical tasks and thus should be verified. We formalize the class of track topology aggregation protocols and provide a parameterized proof of correctness where the problem is reduced to checking a property of the node’s aggregation algorithm. We provide a verification rule based on our property and illustrate the approach by verifying a non-trivial aggregation protocol. %G English %2 https://inria.hal.science/hal-01515244/document %2 https://inria.hal.science/hal-01515244/file/978-3-642-38592-6_4_Chapter.pdf %L hal-01515244 %U https://inria.hal.science/hal-01515244 %~ IFIP-LNCS %~ IFIP %~ IFIP-TC %~ IFIP-WG %~ IFIP-TC6 %~ IFIP-WG6-1 %~ IFIP-FORTE %~ IFIP-DISCOTEC %~ IFIP-LNCS-7892