Abstract-För att underlätta den formella kontrollen av feltoleranta distribuerade protokoll föreslår vi en strategi som avsevärt minskar kostnaderna för deras modellkontroll. Dessa protokoll anger ofta atomära, processlokala händelser som förbrukar en uppsättning meddelanden, ändrar tillståndet för en process och skickar noll eller fler meddelanden. Vi kallar sådana händelser för beslutsmässiga övergångar och utnyttjar dem för att optimera utforskningen av staten på två sätt. För det första skapar vi färre tillstånd jämfört med modeller där beslutsmässiga övergångar uttrycks genom övergångar med enstaka meddelanden. För det andra förfinar vi övergången till en uppsättning likvärdiga, finare kornade övergångar som gör det möjligt för delorderalgoritmer att uppnå bättre reduktion. Vi implementerar MP-Baset modellen checker, som stöder förfinade beslutförhet övergångar. Vi modellerar kontrollprotokoll som representerar grundläggande primitiver av utplacerade tillförlitliga distribuerade system, nämligen: Paxos konsensus, regelbunden lagring, och Bysantine-tolerant multicast. Vi uppnår upp till 92% minne och 85% tidsreduktion jämfört med modellkontroll med standard oraffinerad enkel meddelande övergångar.
Formalisering och verifiering av en klass av feltoleranta distribuerade algoritmer har tagits upp i REF.
Efficient model checking of fault-tolerant distributed protocols
{'venue': '2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN)', 'journal': '2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN)', 'mag_field_of_study': ['Computer Science']}