Durch die zunehmenden Anforderungen an fehlertolerante Protokolle steigt auch deren Komplexität zusehends. Dadurch ist es deutlich schwieriger die Funktionalität der Fehlertoleranzmechanismen zu überprüfen. In dieser Arbeit wird ein modellbasierter Ansatz vorgestellt, dessen Ziel es ist ``Lücken'' in den Fehlertoleranzeigenschaften effizient zu finden. Dazu wird ein Algorithmus entwickelt, der eine partiellen Ordnung erzeugt und es somit erlaubt den Zustandsraum zu verkleinern ohne Verhalten bezüglich der zu prüfenden Eigenschaften zu verlieren. Weiterhin werden zwei Algorithmen zur (partiellen) Analyse entworfen, implementiert und bewertet: Der H-RAFT Algorithmus basiert auf den SDL-Elementen der jeweiligen Transitionen und erfordert keinerlei weiteres Domänen-Wissen des Benutzers. Der Close-to-Failure Algorithmus hingegen ist nur von Benutzerinformationen abhängig. Kombinationen der beiden Ansätze werden ebenfalls untersucht. Für alle vorgestellten Methoden und Algorithmen wird ausgenutzt, dass es sich um fehlertolerante Protokolle handelt. Um die neuen Ansätze mit weitverbreiteten Algorithmen vergleichen zu können wird ein Werkzeug entwickelt, welches eine einfache Integration von Algorithmen ermöglicht. Die vorgestellten Techniken werden ausführlich in Experimenten mit einem Gesamtaufwand von etlichen CPU-Monaten untersucht. Die Ergebnisse dieser Experimentreihen zeigen eindeutig die Vorteile der entwickelten Algorithmen und Methoden.