eSpark Learning, un proveedor de tecnología educativa para escuelas primarias, ejecutaba un proceso de configuración manual y semirregular para cada cliente que coordinaba varios sistemas de terceros y modificaba directamente las redes informáticas de los clientes. A medida que crecía la base de usuarios, la carga de trabajo se volvió insostenible: el equipo de soporte se dio cuenta de que necesitaría una nueva contratación a tiempo completo cada año solo para mantenerse al día. La dirección siempre había considerado que automatizar el proceso era demasiado peligroso: un error podía afectar la red de un cliente y costar el contrato.
El ingeniero Hillel Wayne había usado recientemente la especificación formal (al estilo TLA+) en un proyecto de carga por lotes y había recortado una semana de la entrega al detectar errores de arquitectura antes de escribir código. El gerente de proyecto había definido tres propiedades que el reemplazo automatizado debía garantizar para ser seguro. Wayne modeló el sistema en un lenguaje de especificación y lo ejecutó a través de un verificador de modelos, que simula exhaustivamente cada escenario que permite una especificación y devuelve una traza concreta cuando encuentra uno que infringe una regla.
Tras dos días de modelado, todos los diseños o fallaban de inmediato o contenían un defecto sutil que podía pasar inadvertido en producción durante meses antes de colapsar. Algunos diseños satisfacían dos de las tres propiedades requeridas, pero ninguno satisfacía las tres. En lugar de elegir uno de todos modos y confiar en la suerte, Wayne incorporó al gerente de proyecto a los artefactos de modelado, le mostró de forma concreta cómo fallaría cada diseño y le preguntó de qué propiedad podía prescindir el negocio.
Los expertos en diseño internos determinaron que una propiedad solo necesitaba cumplirse habitualmente, no siempre. Con esa única concesión acotada, el verificador de modelos confirmó que varios diseños ahora funcionarían, y el equipo construyó uno de ellos. El servicio automatizado de configuración funcionó sin incidentes durante años después, sobreviviendo a la permanencia de los ingenieros que lo construyeron.
El verificador de modelos demostró que ningún diseño cumplía las 3 reglas; se negoció una concesión.
Modelar en un lenguaje de especificación es barato de descartar; una base de código casi terminada no lo es, así que probar cada idea de diseño antes de la implementación evitó tiempo de ingeniería desperdiciado.
Un verificador de modelos devuelve una traza de fallo concreta, que resulta más persuasiva para una parte interesada no ingeniera que una advertencia abstracta de riesgo.
Sacar a la luz que «ninguno de estos diseños satisface los tres requisitos» antes de escribir código convirtió un supuesto implícito y no examinado en una decisión explícita que el gerente de proyecto realmente podía tomar.
Cuando todos los diseños que pruebas parecen fallar, modela el espacio formalmente primero. Un verificador de modelos convierte una vaga sensación de riesgo en una concesión específica y negociable que puedes plantear antes de escribir código alguno.
El servicio automatizado de gestión de configuraciones funcionó eficientemente durante años, mucho más allá de la permanencia de los ingenieros que lo construyeron. Wayne pasó a trabajar a tiempo completo como consultor de especificación formal y a escribir sobre la práctica, incluido un libro sobre el tema y trabajo de documentación para el lenguaje de especificación Alloy.
CONSULTA LAS PRUEBAS
Las fuentes
- Planning with flare Increment · increment.com