id: 06229299
dt: a
an: 06229299
au: Bongiovanni, Francesco; Henrio, Ludovic
ti: A mechanized model for CAN protocols.
so: Cortellessa, Vittorio (ed.) et al., Fundamental approaches to software
engineering. 16th international conference, FASE 2013, held as part of
the European joint conferences on theory and practice of software,
ETAPS 2013, Rome, Italy, March 16‒24, 2013. Proceedings. Berlin:
Springer (ISBN 978-3-642-37056-4/pbk). Lecture Notes in Computer
Science 7793, 266-281 (2013).
py: 2013
pu: Berlin: Springer
la: EN
cc:
ut: structured P2P; CAN; broadcast algorithm; theorem proving
ci:
li: doi:10.1007/978-3-642-37057-1_20
ab: Summary: Formal reasoning on Peer-to-Peer (P2P) systems is an intimidating
task. This paper focuses on broadcast algorithms for Content
Addressable Network (CAN). Since these algorithms run on top of complex
P2P systems, finding the right level of abstraction in order to prove
their functional correctness is difficult. This paper presents a
mechanized model for both CAN and broadcast protocols over those
networks. We demonstrate that our approach is practical by identifying
sufficient conditions for a protocol to be correct and efficient. We
also prove the existence of a protocol verifying those properties.
rv: