Extremes Modellieren bei MongoDB: Konformitätsprüfung in der Praxis

MongoDB-Ingenieure experimentierten mit TLA+-Spezifikationen und zwei Konformitätsprüfungstechniken (Trace-Checking und Testfallgenerierung), um zu überprüfen, ob die Implementierungen ihrer Produkte den Spezifikationen entsprechen. Das Trace-Checking-Experiment, durchgeführt auf dem MongoDB-Server, zielte darauf ab, die Implementierung des Raft-Konsensusprotokolls zu validieren; das Testfallgenerierungs-Experiment, auf dem MongoDB Mobile SDK, zielte darauf ab, den Algorithmus der operativen Transformation zu validieren. Die Ergebnisse zeigten, dass das Trace-Checking aufgrund der Schwierigkeit, den Zustand eines Multithreading-Programms zu erfassen, und Diskrepanzen zwischen Spezifikation und Implementierung fehlschlug, während die Testfallgenerierung erfolgreich einen Fehler im Algorithmus aufdeckte und eine 100%ige Zweigabdeckung erreichte. Der Artikel fasst die gewonnenen Erkenntnisse zusammen und präsentiert aktuelle Fortschritte in diesem Bereich, wobei die Bedeutung einer kontinuierlichen Konformitätsprüfung für die allgemeine Akzeptanz von TLA+ hervorgehoben wird.