Abstrakt. Strukturerade peer-to-peer overlay nätverk är en klass av algoritmer som ger effektiv meddelande routing för distribuerade applikationer med hjälp av ett glest uppkopplat kommunikationsnät. I detta dokument verifierar vi formellt en typisk applikation som körs på en fast uppsättning noder. Detta arbete är grunden för studier av ett mer dynamiskt system. Vi identifierar ett värde- och uttrycksspråk för en värdepasserande CCS som gör att vi formellt kan modellera en distribuerad hashtabell som genomförs över ett statiskt DKS overlay-nätverk. Vi ger sedan en specifikation av uppslagsfunktionen på samma språk, vilket gör det möjligt för oss att formellt kontrollera att systemet är korrekt när det gäller observationslikvärdighet mellan genomförande och specifikation. Som bevis använder vi en abstrakt notation för nåbara stater som gör det möjligt för oss att arbeta bekvämt upp till strukturell kongruens, vilket drastiskt minskar antalet och formen av stater att överväga. De korrekta bevisens struktur och tekniker är återanvändbara för andra overlay-nätverk.
En uppslagssalgoritm för det DHT-baserade DCS-systemet har verifierats för en statisk modell av nätverket med hjälp av värdepasserande CCS REF.
Verifying a Structured Peer-to-peer Overlay Network: The Static Case ⋆
{'venue': 'Global Computing', 'journal': None, 'mag_field_of_study': ['Computer Science']}