Parameterized Verification of Track Topology Aggregation Protocols

Abstract : 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.
Complete list of metadatas

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-01515244
Contributor : Hal Ifip <>
Submitted on : Thursday, April 27, 2017 - 10:46:49 AM
Last modification on : Thursday, April 27, 2017 - 2:43:59 PM
Long-term archiving on : Friday, July 28, 2017 - 12:41:22 PM

File

978-3-642-38592-6_4_Chapter.pd...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Sergio Feo-Arenis, Bernd Westphal. Parameterized Verification of Track Topology Aggregation Protocols. 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), Jun 2013, Florence, Italy. pp.35-49, ⟨10.1007/978-3-642-38592-6_4⟩. ⟨hal-01515244⟩

Share

Metrics

Record views

137

Files downloads

143