Modelado Extremo en MongoDB: Verificación de Conformidad en la Práctica

Los ingenieros de MongoDB experimentaron con especificaciones TLA+ y dos técnicas de verificación de conformidad (verificación de rastreo y generación de casos de prueba) para verificar si las implementaciones de sus productos cumplen con las especificaciones. El experimento de verificación de rastreo, realizado en el servidor MongoDB, tuvo como objetivo validar la implementación del protocolo de consenso Raft; el experimento de generación de casos de prueba, en el SDK móvil de MongoDB, tuvo como objetivo validar el algoritmo de transformación operacional. Los resultados mostraron que la verificación de rastreo falló debido a la dificultad de tomar instantáneas del estado de un programa multiproceso y discrepancias entre la especificación y la implementación, mientras que la generación de casos de prueba descubrió con éxito un error en el algoritmo y logró el 100% de cobertura de ramificación. El artículo resume las lecciones aprendidas y presenta avances recientes en el campo, destacando la importancia de la verificación continua de conformidad para la adopción generalizada de TLA+.